基于符号执行提高缺陷分析的精确性研究

摘要

静态分析是发现软件源代码缺陷和提高软件源代码质量的有效方式.然而,静态分析由于不实际运行代码,无法收集足够的数据流信息,故其分析结果存在精确性偏低的情况.符号执行技术通过模拟程序的执行能够收集足够的数据流信息,从而增加数据流分析的精确性,弥补静态分析工具的缺陷.为了提高静态分析结果的精确性,本文设计并实现了一个源代码缺陷检测工具ABAZER-SE,它基于GCC抽象语法树,组合采用符号执行与静态分析技术以检测源代码中的缺陷.使用Toyota ITC静态分析基准对该工具进行了评估,实验结果表明,本文方法及工具可以提高静态分析检测结果的精确性.