Imperial College London
Professor Cristian Cadar

ProfessorCristianCadar

Faculty of Engineering, Department of Computing

Professor of Software Reliability
 
 
 
//

Contact

 

c.cadar Website

 
 
//

Location

 

435Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Busse:2022:10.1145/3533767.3534384,
author = {Busse, F and Gharat, P and Cadar, C and Donaldson, A},
doi = {10.1145/3533767.3534384},
pages = {568--579},
publisher = {ACM},
title = {Combining static analysis error traces with dynamic symbolic execution (experience paper)},
url = {http://dx.doi.org/10.1145/3533767.3534384},
year = {2022}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - This paper reports on our experience implementing a techniquefor sifting through static analysis reports using dynamic symbolicexecution. Our insight is that if a static analysis tool produces apartial trace through the program under analysis, annotated withconditions that the analyser believes are important for the bugto trigger, then a dynamic symbolic execution tool may be ableto exploit the trace by (a) guiding the search heuristically so thatpaths that follow the trace most closely are prioritised for explo-ration, and (b) pruning the search using the conditions associatedwith each step of the trace. This may allow the bug to be quicklyconfirmed using dynamic symbolic execution, if it turns out to be atrue positive, yielding an input that triggers the bug.To experiment with this approach, we have implemented the ideain a tool chain that allows the popular open-source static analysistools Clang Static Analyzer (CSA) and Infer to be combined withthe popular open-source dynamic symbolic execution engine KLEE.Our findings highlight two interesting negative results. First, whilefault injection experiments show the promise of our technique,they also reveal that the traces provided by static analysis tools arenot that useful in guiding search. Second, we have systematicallyapplied CSA and Infer to a large corpus of real-world applicationsthat are suitable for analysis with KLEE, and find that the staticanalysers are rarely able to find non-trivial true positive bugs forthis set of applications.We believe our case study can inform static analysis and dynamicsymbolic execution tool developers as to where improvements maybe necessary, and serve as a call to arms for researchers interestedin combining symbolic execution and static analysis to identifymore suitable benchmark suites for evaluation of research ideas.
AU  - Busse,F
AU  - Gharat,P
AU  - Cadar,C
AU  - Donaldson,A
DO  - 10.1145/3533767.3534384
EP  - 579
PB  - ACM
PY  - 2022///
SP  - 568
TI  - Combining static analysis error traces with dynamic symbolic execution (experience paper)
UR  - http://dx.doi.org/10.1145/3533767.3534384
UR  - http://hdl.handle.net/10044/1/97427
ER  -
Download