多遍目标导向动态符号执行

动态符号执行（DSE）提供了一种精确的程序分析手段，可用于生成测试用例并检测多种缺陷，包括内存漏洞。然而，路径爆炸问题可能阻止符号执行器覆盖程序中感兴趣的位置或路径。在本文中，我们提出了一种多遍目标导向动态符号执行方法，该方法从目标程序位置出发向后搜索，直至到达指定的入口点以检查可达性，检测入口点与目标之间可行路径上的缺陷，并收集代码访问的内存位置约束。我们的方法混合了反向推理与前向推理遍。它引入了一个抽象地址空间，在反向遍期间被填充，并使用合一（unification）将抽象对象精确映射到具体地址空间中的对象。我们使用DSE工具KLEE实现了名为DESTINA的工具。我们使用SvComp内存安全和控制流类别的基准对DESTINA进行了评估。结果表明，DESTINA能够精确检测内存漏洞，并且能够在DSE因路径爆炸而难以到达目标位置时帮助其更快地到达目标位置。我们的方法平均将探索的路径数减少了4倍，将速度提升了2倍。