My Work at Imperial
- Topic
Sifting Through Static Analysis Reports Using Dynamic Symbolic Execution: from Error Traces to Bug-Triggering Test Cases- More details
We propose an approach to automate the process of confirming potential bugs reported by static analysis. Given a bug report from a static analysis tool, we use dynamic symbolic execution (DSE) to try to automatically generate an input that triggers the reported bug.
More precisely, our technique works as follows. Suppose a static analyser reports a possible bug at a given program location. The analyser typically yields a trace providing (possibly incomplete) details of a path through the program that, if followed, might trigger the bug. Our idea is to then apply a DSE tool to the program, additionally providing the DSE tool with information related to the trace. Rather than attempting to explore all paths of the program in the hope of finding some bug, the DSE tool exploits the trace to explore a massively-pruned subset of paths that agree with the trace, with the aim of confirming the specific bug reported by the static analyser. Our hypothesis is that---if the bug turns out to be a true positive---the DSE tool may be able to confirm the bug, producing an associated triggering test case, more efficiently than if it were run on the program in a default, undirected fashion. If the DSE tool is unable to trigger the bug then we still don't know whether the bug report is a true or a false positive (except in the extreme case where DSE is able to fully explore the program), but we can de-prioritize that report in favour of other reports that are confirmed.
We present a general strategy for integrating a DSE tool with a trace-producing static analyser via a new intrinsic function, klee_assume_sa, that allows the sequence of steps of the static analysis trace to be encoded in the program under analysis, together with conditions that the static analyser believes should hold at each step. We propose three strategies for handling the conditions associated with calls to klee_assume_sa: ignore, which treats these conditions as no-ops; require, which aggressively prunes the search space by terminating exploration of a path as soon as a condition is found to be infeasible; and try, which adds a feasible condition to the current path condition but ignores it otherwise. We also propose a novel search heuristic that uses the klee_assume_sa functions associated with a static analysis trace to prioritise exploration of paths that follow the trace.