An Improved Offline Symbolic Execution Approach

The offline symbolic execution technique generates a trace file by actually executing the program, and then the path constraint of a branch in the trace file is flipped and solved to generate a new sample. Since the offline symbolic execution technique analyzes only one path at a time, it occupies less memory resources. However, when the program has many branches, the offline symbolic execution technique has a problem of low execution efficiency. This paper proposes a visualized and distributed offline symbolic execution approach (VDO), which mainly improves the efficiency of offline symbolic execution technique from three aspects. Firstly, VDO only flips the branches of the specified range, so that it can reduce the flipping of branches with low test value and improve the pertinence of the test. Second, VDO uses the sample sequence number as the color value in the global control flow graph to visualize the branch that have been traversed, so that it can find the input sample corresponding to each branch, and can preferentially select those branches that have not been traversed for flipping. Finally, VDO disassembles the offline symbolic execution process into three phases, and builds a distributed pipeline based on the finite state machine to further increase efficiency. In order to evaluate VDO, we implemented this approach based on the BAP platform. The results of testing coreutils and the LAVA-M dataset showed that coverage increased by an average of more than 13%, and the total number of discovered vulnerabilities increased by 15 compared to the original BAP platform.