EXE: Automatically Generating Inputs of Death
From GradTurkey
[edit] Summary
EXE is a bug finding tool which tries to bridge the gap between static and dynamic analysis. Traditional dynamic analysis suffers from poor coverage of the code available; static analysis has complete path coverage, but
"reasons poorly about bugs that depend on accurate value information (the exact value of an index or size of an object), pointers, and heap layout, among many others."
The EXE tool uses a combination of symbolic and concrete execution to derive constraints on user specified inputs. When executing if-statements that involve symbolic values, the tool forks into two copies -- one where the if-statement is constrained to true, and one where the if-statement is constrained to false. Whenever the program might terminate (through an assertion failure or normal termination), a custom constraint solver is invoked to find concrete inputs that exercise the exact path being considered by EXE. Thus, the tool also acts as a test generator to exercise each path through the program.
Another contribution of the paper is the constraint solver, STP. It has primitives that allow constraints to be added for all C expressions (except floating point), and is highly optimized for reasoning about arrays. The paper provides good details on the implementation of STP, which transforms expressions into predicates and uses an off-the-shelf SAT solver to find constrained inputs.
