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

Full-automatic Detection of Memory Safety Violations for C Programs

作　　者：杨飏[1] 张焕国[1,2,3] 王后珍[1] 

机构地区：[1]空天信息安全与可信计算教育部重点实验室,武汉430072 [2]武汉大学计算机学院,武汉430079 [3]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机科学》2010年第6期155-158,185,共5页Computer Science

基　　金：国家863高技术研究发展计划项目基金(2007AA01Z411;2008AA01Z404);国家自然科学基金(90718005;90718006)资助

摘　　要：符号执行是目前较为行之有效的软件缺陷自动化检测方法,计算代价昂贵与程序执行路径爆炸是两个影响其性能的关键问题。提出了一种针对C语言程序内存访问缺陷的符号执行检测方法,该方法可通过自动化构造的测试用例发现程序内部的内存访问缺陷,如缓冲区溢出、跨界访问和指针异常等。使用符号跟踪缓冲区长度的方法,一方面减少了符号变量的数量,另一方面由此精确抽象C语言库中字符串操作函数的行为,解决了符号执行过程间函数调用的步进问题;使用动态切片的方法,裁减路径探索过程中的冗余路径,从而解决在程序内部路径搜索时发生的路径爆炸问题。实验表明,提供的检测方法不但可行,而且验证代价较小,具有较强的实用性。Symbolic execution is an effective and automatic bug-finding method. But symbolic execution is limited in practice by the computation cost and path explosion. We presented a tool for full-automatic detection and generating inputs that lead to memory safety violations in C programs, including buffer overflow, buffer overrun and pointer dereference error. In order to reduce the amount of symbol variable, we used the symbol variable to track the length of buffer and C string. The use of symbolic buffer length makes it possible to compactly summarize the behavior of standard buffer manipulation functions. While resolving the problem of path explosion, we introduced the dynamic slicing methods to prune the redundant paths. It＇s shown by the experiments that our method presented in this paper not only is feasible but also has little cost.

关 键 词：静态分析 符号执行 程序切片 约束求解 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]