A Dynamic Symbolic Execution Tool For X86 Binary Programs

Program analysis is playing an important role in the field of computer security. It is useful for the evaluation of both applications and operating system. Nowadays, there are many program analysis approaches. Taint analysis and symbolic execution have been the most popular and effective technique among the others. Typically, symbolic execution is more precise than the taint analysis, and becomes the great research topic in the field of program analysis all over the world.Traditional symbolic execution replaces the concrete variables with symbols, and runs the program. At the branch instruction, symbolic execution establishes a constraint, and gathers all the constraints to form a path condition along the program path. The program input that satisfies such a path condition can lead the program to the corresponding path.However, traditional symbolic execution suffers from several severe problems such as state explosion, complex mathematical constraints, low efficiency, etc. In order to tackle those problems, we present a lightweight dynamic symbolic execution tool, LDSE. LDSE mixes dynamic and symbolic execution, and deploys the dynamic backward program slicing to effectively relieve the existing issues. LDSE introduces four contributions:1) A compact unified memory model.2) Instruction cache.3) Dynamic backward program slicing.4) A lightweight dynamic symbolic execution framework for x86 programs.Our experiment results show that the lightweight dynamic symbolic execution tool can be applied in both testcase generation and program path coverage. Typically, dynamic backward program slicing makes the symbolic execution degrade gracefully.