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.