基于GCC的符号执行工具

The Symbolic Execution Tool Based on GCC

静态分析和符号执行是发现源代码缺陷和提高源代码质量的两种有效方式。然而,这两种技术都面临各自的问题,静态分析误报率较高和符号执行一直面临着路径爆炸难题。为了减少静态分析和符号执行的这些限制,本文构建了一个称为ABARZER-SE的工具,它是第一个基于GCC结合符号执行和静态分析的源代码检测工具。ABAZER-SE由两个阶段组成,第一阶段是通过符号执行获取可行性路径,第二阶段应用静态分析技术对可行性路径分析找到源代码中缺陷。实验结果表明该工具具有可行性、有效性和可扩展性。

Static analysis and symbolic execution are two powerful ways of finding bugs and improving the quality of software. However, both of these techniques face their respective issues, e.g. false positives with static analysis tools and path explosion with symbolic execution method. To mitigate these limitations of static analysis and symbolic exe-cution, we present a tool called ABARZER-SE, which is the first to implement symbolic execution and static analysis based on GCC. The workflow of ABAZER-SE consists of two phases, the first phase is to achieve feasible path by us-ing symbolic execution, the second combines static analysis to analyze potential bugs. Experiment results show the ef-fectiveness and scalability of the tool when it is used to analyze real-world software.