道路缺陷自动检测程序

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