static-analysis - 可达性和符号执行

Question

现在我对符号执行（SE）和可达性分析（RA）感到困惑。据我所知，SE 使用符号来执行一些代码以到达具有分支条件的每个分支。而且 RA 可以用来查找每个分支的可达性，对吧？当使用 RA 时，我们可以提取每个分支的分支条件。如果是这样，它们之间有什么区别？他们能快点吗？都是静态分析吗？

谢谢，夏娃

Answer 1

可达性分析主要用于查看模型是否可以达到某个状态。然而，符号执行是一种静态分析技术（有时也是动态的，就像 KLEE 所做的那样），用于查找程序/源代码中的所有路径。

Answer 2

符号执行是在不执行程序的情况下完成的。因此，它是静态分析。

一个好的符号分析将计算每个程序点的路径条件。一个更好的人将能够推理路径公式，以证明它是可行的（程序点可到达）或不可行（程序点已死）。

与编译代码的执行速度相比，符号执行往往很慢。

Answer 3

符号执行不是静态的，它以符号方式执行程序。出于性能的考虑，像 klee 这样的符号执行工具在遇到分支时并没有解决分支条件。它使用廉价的分析来查看它是否可能是可访问的。当到达程序的出口时，它将尝试生成一个测试用例。如果收集到的从起点（主函数）到出口的约束条件满足，则给出一个测试用例，否则出口不可达。SE 使用可达性分析来生成覆盖代码的测试用例。