一种C程序内存访问缺陷自动化检测方法研究

被引：3

作者：

杨飏 ^{[1
]}

张焕国 ^{[1
,2
,3
]}

王后珍 ^{[1
]}

机构：

[1] 空天信息安全与可信计算教育部重点实验室

[2] 武汉大学计算机学院

[3] 武汉大学软件工程国家重点实验室

来源：

计算机科学 | 2010年 / 37卷 / 06期

关键词：

静态分析; 符号执行; 程序切片; 约束求解;

D O I：

暂无

中图分类号：

TP311.53 [];

学科分类号：

081202 ; 0835 ;

摘要：

符号执行是目前较为行之有效的软件缺陷自动化检测方法,计算代价昂贵与程序执行路径爆炸是两个影响其性能的关键问题。提出了一种针对C语言程序内存访问缺陷的符号执行检测方法,该方法可通过自动化构造的测试用例发现程序内部的内存访问缺陷,如缓冲区溢出、跨界访问和指针异常等。使用符号跟踪缓冲区长度的方法,一方面减少了符号变量的数量,另一方面由此精确抽象C语言库中字符串操作函数的行为,解决了符号执行过程间函数调用的步进问题;使用动态切片的方法,裁减路径探索过程中的冗余路径,从而解决在程序内部路径搜索时发生的路径爆炸问题。实验表明,提供的检测方法不但可行,而且验证代价较小,具有较强的实用性。

引用

页码：155 / 158+185 +185

页数：5