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

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

Full-automatic Detection of Memory Safety Violations for C Programs

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.