王眉林，张旖旎，李明月，邵帅，刘湿润

(1.中国信息安全测评中心，北京 100085；2.北京邮电大学 计算机学院，北京 100876)

静态分析是一种重要的程序分析方法，国内外已有大量基于静态分析查找程序错误的研究[1]. 然而，由于静态分析不实际执行代码，无法收集足够数据流信息，导致分析结果的准确性相对较低. 符号执行也是一种程序分析技术，其核心思想是利用符号值代替变量的实际值模拟程序的执行，常用于软件测试和检测软件漏洞. 大部分符号执行工具基于更底层的编译器中间表示进行分析，包含有更多的源代码信息，具有较高的分析精度. 有研究表明，使用符号执行能够分析源代码中的严重缺陷，并可生成高覆盖率测试用例[1].

本文提出了基于符号执行技术提高静态分析检测结果准确性的方案，其核心思想是通过符号执行，收集足够数据流信息，以弥补传统静态分析的缺陷，并开发了源代码缺陷分析工具ABAZER-SE，主要工作包括：

① 设计并实现源代码缺陷分析工具ABAZER-SE，使用抽象语法树对程序代码进行静态分析，并结合符号执行技术提升分析精度和效率. 通过构建分层的内存模型，实现了对源代码语义的精确模拟;

② 采用Toyota ITC基准数据对本文研发的工具进行了评估和对比实验，结果表明，该工具有较高的缺陷分析精度.

1 设 计

1.1 目 标

本项研究有两个目标，一是通过符号执行，识别不可达路径以提高数据流分析的准确性；二是探索在GCC平台上实现……