Dynamic symbolic execution (DSE) provides a precise means to analyze programs and it can be used to generate test cases and to detect a variety of bugs including memory vulnerabilities. However, the path explosion problem may prevent a symbolic executor from covering program locations or paths of interest. In this paper, we present a Multi-Pass Targeted Dynamic Symbolic Execution approach that starts from a target program location and moves backward until it reaches a specified entry point to check for reachability, to detect bugs on the feasible paths between the entry point and the target, and to collect constraints about the memory locations accessed by the code. Our approach uses a mix of backward and forward reasoning passes. It introduces an abstract address space that gets populated during the backward pass and uses unification to precisely map the abstract objects to the objects in the concrete address space. We have implemented our approach in a tool called DESTINA using KLEE, a DSE tool. We have evaluated DESTINA using SvComp benchmarks from the memory safety and control-flow categories. Results show that DESTINA can detect memory vulnerabilities precisely and it can help DSE reach target locations faster when it struggles with the path explosion. Our approach achieves on average 4X reduction in the number of paths explored and 2X speedup.

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