Anxtiety. Dynamic program analysis tool
Dynamic symbolic execution
Automatic defect detection
Dynamic symbolic execution is a method of automatic input data generation for target program without knowledge of its internal structure and semantics; generated input data is used to traverse execution paths and attempt to force defects caused by dangerous operations. Dynamic symbolic execution incorporates a number of steps that are performed iteratively: execute the target program and form an execution path constraint using a set of input data, then process the generated path constraint with the help of a solver in order to construct new sets of input data to reach previously uncovered areas of code or trigger dangerous operations. The most promising set for the next iteration is selected according to the amount of new, previously unknown basic blocks it covers.
Input data sets can simulate various input sources: files, network interfaces (sockets), command line arguments and environment variables. The following runtime defects can be detected: assert violations, division by zero, null pointer dereference, and infinite loops.
Anxiety uses DynamoRIO, PIN, Dyninst and Valgrind instrumentation frameworks to construct path constraint. We have developed custom Valgrind plugins to generate path constraints and track coverage of basic blocks. For the other frameworks we use Triton to handle the instruction flow.
Anxiety uses SMT-solvers to process path constraint and generate input data; supported solvers include prominent state-of-the-art solutions such as STP, Z3, MathSAT and others.
Potential defect evaluation
Dynamic symbolic execution can be used to evaluate potential defects reported by an analyst or identified with the help of static analysis tools.
Static analysis is used to annotate nodes of a control flow graph with distance to a dangerous operation. Such annotations could be used to guide symbolic execution.
It is possible to construct an input data set which will trigger given dangerous operation by enforcing partial path constraint during dynamic symbolic execution.
Reaching target code points
Dynamic symbolic execution can be used to construct a data set that will force program execution to reach a certain point in code. This feature can be used to supplement program fuzzing in order to pass through conditional instructions in a required way.
Fuzzing is a technique for automatic input data set generation; typically it is more efficient in building program coverage than dynamic symbolic execution. In order to generate input data sets fuzzing relies on lightweight algorithms: genetic, pseudo-random, or algorithms that use information about internal program structure.