Ivannikov Institute for System Programming of the RAS


Anxtiety. Dynamic program analysis tool

Dynamic symbolic execution

Anxtiety. Dynamic program analysis tool

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.

Instrumentation

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.

Solvers

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.

Reachability

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.

Anxtiety. Dynamic program analysis tool

Directed analysis

It is possible to construct an input data set which will trigger given dangerous operation by enforcing partial path constraint during dynamic symbolic execution.

Anxtiety. Dynamic program analysis tool

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

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.

Anxtiety. Dynamic program analysis tool

Developer/Participant

Compiler Technology

Back to the list of technologies of ISP RAS