开发者撰文解释静态分析的基本概念与取舍

很多开发者都听说过“静态分析”这个词，以及“健全性”和“程序语义”等相关术语，但这些概念究竟是什么意思、彼此之间如何关联，却并不总是那么清楚（至少对曾经的我是这样）。本文介绍这些基本术语及其背后的直觉。我们先从静态分析能提供什么、它如何弥补测试和代码审计的局限谈起，然后探讨它的局限：为什么不可判定性使得近似成为必要，以及设计有用分析时涉及的权衡，并在此过程中解释健全性、完备性和精确性等概念。这篇博文改编自我博士论文中的材料，如果需要更多细节可以查阅原文。

软件保障的常见做法是测试和代码审计。测试的核心是在一组输入上运行程序，并确认其行为符合预期。当测试失败时，开发者会调查原因并修复，然后重新运行测试套件（也许还会根据调试中的发现补充更多测试，从而提升对程序正确性的信心）。测试的好处在于：如果它发现了 bug，那就是真正的 bug——不会有误报！缺点则是测试并不穷尽：一般来说，无论执行多少测试，测试都无法探索程序在运行时可能走的所有执行路径。

代码审计本质上就是说服自己（或你的客户/老板/同事）代码是正确的。相比测试，一个明显优势是：人在阅读代码时可以概括、推断事实并建立联系，这有助于他们同时推理多次执行。然而，和测试一样，代码审计既耗时，归根结底也仍然不穷尽（无论审查代码的人多么聪明、多么专注，总有可能漏掉某些东西）。

这是不是问题，可能取决于应用领域。我不是游戏开发者，但我猜想，如果游戏中的某个 bug 导致屏幕上某个像素偶尔黑屏一瞬间，那也许没什么大不了。或者如果网页偶尔加载不出来、用户需要刷新一下（前提是没有丢失重要数据！），我想那也没什么大不了。但在音频软件中，同类的故障却可能不可接受：哪怕一个音频采样出错，都可能产生爆音（相信我，没人愿意在舞台上或录音中听到这种声音）。在智能合约中，bug 可能被利用来耗尽协议中的所有资金（这种情况已经发生过多次，造成数百万美元损失）；网站中的 bug 则可能使其暴露于攻击之下，导致用户数据泄露或被破坏。由此可见，在多个领域中，研究尽可能考虑更多执行路径（或者确实考虑所有执行路径）的技术其实非常有用（而不只是学术练习）。

静态分析就是这样一种技术。它通过自动分析程序来工作，而不运行程序。在这一点上它类似于代码审计，但审查不是由人执行，而是由程序——静态分析器——执行。这有一个重要优势：静态分析能够比测试和代码审计提供更高的覆盖率，在某些情况下甚至可以探索程序中的所有可能执行路径，并保证不存在错误。然而，如果你觉得这听起来好得不像真的，你并没有错。事实上，上述好处是有代价的：静态分析器只能检查有限（而且通常简单）的性质；它们可能漏掉错误、发出误报，还可能耗时且资源密集。我们将在本文剩余部分进一步探讨这一点。

静态分析是一种算法，它以程序为输入，试图回答关于程序可能运行时行为集合（通常称为其语义）的某个问题。典型问题包括：

不幸的是，对任意程序自动且精确地回答这些问题，是不可判定的。为了说明这一点，我们需要退一步，考虑“经典的”静态分析问题：停机问题。设 P 为任意程序。P 是否在所有输入上终止？我们能否设计一个算法，对任意程序回答这个问题？不幸的是，答案是否定的：可以证明，这种算法的存在会导致逻辑矛盾，因此我们必须得出结论：该算法本身不可能存在。如果你想了解更多，我在之前的一篇博文中讨论过这个话题。此外还可以证明，许多有趣的静态分析问题，包括上面的例子，至少和停机问题一样难，因此也是不可判定的。我们这里不展开细节（你可以在我的博士论文第 4 章找到更多内容），但关键思想是：假设我们有这样一个分析器，能够对任意程序精确回答这些问题之一，并考虑所有可能输入；那么可以证明，这个分析器也可以用来解决停机问题；换句话说，该分析和停机问题在某种程度上“难度等价”。但既然我们已经知道停机问题无法解决，那就必须得出结论：我们的分析也不可能存在。

那我们要放弃吗？不！这些限制只是告诉我们，精确的静态分析是不可能的，但有用的静态分析仍有很大空间。通过接受某种近似，并谨慎处理一些关键的设计权衡，我们可以构建在实践中真正有用的分析（尽管并不精确/完美）。那么这种近似在实践中是什么样子？它通常表现为以下方面的组合：

上面简要讨论的不可判定性结果表明，必然存在某种近似；

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）