Combining static analysis error traces with dynamic symbolic execution (experience paper)

File Description SizeFormat 
sa-dse-issta22.pdfAccepted version713.14 kBAdobe PDFView/Open
Title: Combining static analysis error traces with dynamic symbolic execution (experience paper)
Authors: Busse, F
Gharat, P
Cadar, C
Donaldson, A
Item Type: Conference Paper
Abstract: This paper reports on our experience implementing a technique for sifting through static analysis reports using dynamic symbolic execution. Our insight is that if a static analysis tool produces a partial trace through the program under analysis, annotated with conditions that the analyser believes are important for the bug to trigger, then a dynamic symbolic execution tool may be able to exploit the trace by (a) guiding the search heuristically so that paths that follow the trace most closely are prioritised for explo- ration, and (b) pruning the search using the conditions associated with each step of the trace. This may allow the bug to be quickly confirmed using dynamic symbolic execution, if it turns out to be a true positive, yielding an input that triggers the bug. To experiment with this approach, we have implemented the idea in a tool chain that allows the popular open-source static analysis tools Clang Static Analyzer (CSA) and Infer to be combined with the popular open-source dynamic symbolic execution engine KLEE. Our findings highlight two interesting negative results. First, while fault injection experiments show the promise of our technique, they also reveal that the traces provided by static analysis tools are not that useful in guiding search. Second, we have systematically applied CSA and Infer to a large corpus of real-world applications that are suitable for analysis with KLEE, and find that the static analysers are rarely able to find non-trivial true positive bugs for this set of applications. We believe our case study can inform static analysis and dynamic symbolic execution tool developers as to where improvements may be necessary, and serve as a call to arms for researchers interested in combining symbolic execution and static analysis to identify more suitable benchmark suites for evaluation of research ideas.
Issue Date: 1-Jul-2022
Date of Acceptance: 8-Apr-2022
URI: http://hdl.handle.net/10044/1/97427
DOI: 10.1145/3533767.3534384
ISBN: 9781450393799
Publisher: ACM
Start Page: 568
End Page: 579
Journal / Book Title: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis
Copyright Statement: © 2022 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ISSTA 2022: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (July 2022) https://doi.org/10.1145/3533767.3534384
Sponsor/Funder: DSO National Laboratories
European Research Council (ERC)
Engineering & Physical Science Research Council (E
Funder's Grant Number: DSOCO16080
819141
Ref: 542716
Conference Name: International Symposium on Software Testing and Analysis (ISSTA 2022)
Publication Status: Published
Start Date: 2022-07-18
Finish Date: 2022-07-22
Conference Place: Virtual, South Korea
Appears in Collections:Computing
Faculty of Engineering