Directed Symbolic Execution Tool Based on Clang Static Analyzer: Efficient and Accurate Verification of Static Analysis Results

Directed Symbolic Execution Tool Based on Clang Static Analyzer: Efficient and Accurate Verification of Static Analysis Results

연구 분야: Verification

학회: International Conference on Cyberspace Simulation and Evaluation

This paper implements a static directed symbolic execution tool based on Clang Static Analyzer, which verifies the analysis results of other C/C++ static analysis tools to determine the authenticity of the existence of vulnerabilities. The tool maps the bug traces at the source code level to the control flow graph by parsing the vulnerability reports output from other static analysis tools, and completes the discrete bug traces into continuous ones by analyzing the dependencies of the basic blocks, and finally filters the target blocks to be analyzed in the worklist algorithm, which effectively reduces the analysis of irrelevant code. Experiments show that compared with Infer, the proposed method reduces the false positives of two types of vulnerability codes, CWE407 and CWE457, to 42.5 and 16.9 of the original ones on Juliet C/C++ 1.3, respectively, and eliminates the false positives in CWE476. Directed symbolic execution is on average 9.7 times more efficient compared to full-volume analysis.