validation - 静态分析与实现中的符号执行

Question

静态分析的实现和符号执行有什么区别？

Answer 1

静态分析是检查代码并产生关于代码质量的意见的任何离线计算。您可以将其应用于源代码、Java/C#/... 虚拟机指令集的虚拟机代码，甚至二进制目标代码。没有“一个”静态分析（尽管经典的编译器控制和数据流经常作为 SA 的基础机制突出显示）；该术语共同适用于可能离线使用的所有类型的机制。

符号执行是一种特殊类型的离线计算，它通过构建表示程序在各个点的状态的公式来计算程序实际执行的一些近似值。它被称为“符号”，因为近似值通常是某种涉及程序变量及其值的约束的公式。

静态分析可以使用符号执行并检查结果公式。或者它可能会使用一些其他技术（正则表达式、经典编译器流分析......）或某种组合。但静态分析不必使用符号执行。

符号执行可能仅用于显示计算的预期符号结果。这不是上述定义的静态分析，因为没有任何关于结果有多好的意见。或者，可以对公式进行分析，此时它成为静态分析的一部分。作为一个实际问题，人们可以使用其他程序分析技术来支持符号执行（“这个变量公式被传播到变量 x 的哪个读取？”是一个通常可以通过流分析很好地回答的问题）。

您可能会坚持静态分析是对源代码的任何离线计算，此时符号执行只是一种特殊情况。我认为这个定义没有帮助，因为它不能很好地区分用例。

Answer 2

我真的很喜欢Julian Cohen 在当代自动程序分析演讲中的这张幻灯片。简而言之，人们喜欢将程序分析分为静态分析和动态分析两大类。但是确实有广泛的程序分析技术，从静态到动态，从手动到全自动。符号执行是一种有趣的技术，它介于静态和动态分析之间，通常用作全自动方法。