Abstract: Aiming at the problem that the resource consumption of symbolic execution is too large, this paper proposes an intra-procedural analysis method which is named modeling execution path as process, and combines using the method of modeling objects which is named lazy initialization. A tool prototype which can detect the vulnerability of C code is implemented, and analyzes the Intermediate Rresent(IR) of Phoenix as the direct object. Some known vulnerabilities of Openssl and Apache are verified, and a DOS vulnerability of the version 1.11.4 of wget is detected.

Key words: symbolic execution, static analysis, C code, vulnerability detection

摘要： 针对符号执行分析方法路径资源消耗过大的问题，提出执行路径建模进程化的过程内分析优化方法。结合基于惰性初始化的对象建模方法，以Phoenix编译器中间表示层的代码作为直接分析对象，实现一个检测C代码漏洞的工具原型。使用该工具验证了Openssl和Apache软件的已知漏洞代码，并在wget的1.11.4版本中发现一个“拒绝服务”漏洞。

关键词: 符号执行, 静态分析, C代码, 漏洞检测

CLC Number: 

• TP309.2