An Approach to Reachability Determination for Static Analysis Defects with the Help of Dynamic Symbolic Execution

Аннотация

Program analysis methods for error detection are conventionally divided into two groups: static analysis methods and dynamic analysis methods. In this paper, we present a combined approach that allows one to determine reachability for defects found by static program analysis techniques through applying dynamic symbolic execution to a program. This approach is an extension of our previous approach to determining the reachability of specific program instructions by using dynamic symbolic execution. The approach is sequentially applied to several points in the program: a defect source point, a defect sink point, and additional intermediate conditional jumps related to a defect under analysis. Our approach can be briefly described as follows. First, static analysis of the program executable code is carried out to gather information about execution paths that guide dynamic symbolic execution to the source point of a defect. Then, dynamic symbolic execution is performed to generate an input dataset for reaching the defect source point and the defect sink point through intermediate conditional jumps. Dynamic symbolic execution is guided by the heuristic of the minimum distance from the previous path to the next defect trace point when selecting execution paths. The distance metric is computed using an extended call graph of the program, which combines its call graph and portions of its control flow graph that include all paths leading to the defect sink point. We evaluate our approach by using several open-source command line programs from Debian Linux. The evaluation confirms that the proposed approach can be used for classification of defects found by static program analysis. However, we found some limitations that prevent deploying this approach to industrial program analyzers. Mitigating these limitations is one of the possible directions for future research.