关于形式验证智能合约的五个神话

很长一段时间以来，我一直困惑于如此昂贵、前沿的东西如何可以如此无用，后来我意识到，计算机是一台愚蠢的机器，能够做出令人难以置信的聪明的事情，而计算机程序员是聪明的人，能够做出令人难以置信的愚蠢的事情。简而言之，他们是完美的搭配。

— 比尔·布赖森，作家，摘自《来自大国的笔记》

形式验证使用数学模型和计算机算法来证明或反驳系统设计是否符合表示为属性的正式规范。形式验证是计算机科学的一个成熟领域。鉴于一个程序，我们希望像证明数学定理一样证明该程序是正确的并在预期的方式中运行。或者，目标是展示代码是否存在违反其形式验证的场景。形式验证的理论可以追溯到1949年的艾伦·图灵。在过去的三十年中，该领域显著进展，交互式定理证明器、静态程序分析器和数学约束求解器等工具使得以前仅存在于概念中的验证变得可能，有时甚至根本不存在。随着技术的完善和技术障碍的消失，行业采纳也随之增长。硬件验证领域已经整合了形式验证，防止芯片中的错误，并在各行业中节省了大量资金。

最近，构建工具以正式验证智能合约变得可行。智能合约中的错误可能代价高昂而且难以修复，因为代码是不可变的。形式验证可以防止这些灾难性的错误。

神话 1：证明与错误

“程序测试可以用来显示错误存在，但永远无法证明错误不存在！”

― 埃德斯格·迪克斯特拉

关于形式验证技术的一个非常普遍的看法是，它们仅在代码成熟后有助于证明错误的缺失。然而，可以说，形式验证最令人兴奋的应用是防止在实施过程中出现安全漏洞。像 CBMC 这样的模型检测工具突出了这一能力。由像 Certora Prover 这样的形式验证工具展示，通过将代码与其需求进行比较，在代码部署前后发现错误。

当形式验证工具在开发过程中发现违反要求的潜在测试案例时，就有机会在造成任何伤害之前修正程序。这些错误往往不会上新闻，因为它们永远没有机会在野外被发现。显然，当工具证明一个属性成立时也是有帮助的，但这些实例需要特别的谨慎，以确保被验证的属性描述了正确的行为。

在部署后发现的错误可能更具影响力，甚至是灾难性的。例如，MakerDAO 团队最近通过 Certora Prover 发现 Maker 协议的基础不变量并不是不变量 https://mobile.twitter.com/Kurt_M_Barry/status/1537419724426031106

神话 2：形式验证中最复杂的问题是其计算成本

“对于数学家来说，没有 Ignorabimus，在我看来，自然科学也没有这样的事情。……没人能成功找到无法解决的问题，原因在于，在我看来，没有无法解决的问题。与愚蠢的 Ignorabimus 相反，我们的信条是：我们必须了解，我们将会了解！”

— 大卫·希尔伯特

Rice 定理 证明了计算机程序不可能自动验证任意程序的有趣属性，因此计算机始终无法验证某些程序的正确性。因此，证明即使是极小程序的成本也可以是巨大的。因此，容易认为计算成本是采用和实施形式验证的限制因素。

实际上，形式验证中更大的问题是定义软件所需的属性。Certora倡导的做法，遵循 迪克斯特拉，是让程序员表达关于程序的所需不变量。然而，表达既正确又足够强大的不变量，以找到代码中多种可能的错误是具有挑战性的。

Trident 协议有一个这样的属性示例。Trident 实现了一个流动性池 (LP)，这是一个结构，用户称为流动性提供者向其中添加资金以创建市场。作为交换，保持他们资金在池中的流动性，提供者可以根据其在总流动性中所占的份额从交换活动中获得费用。如果他们决定撤回流动性，提供者可以赎回其份额以收回基础资金。

该系统的属性是流动性和 LP 份额必须都是零，或者它们必须都是非零。换句话说，如果池中存在任何资金，则应存在LP份额，因为有人为该池提供流动性。这个属性是一个不变量的例子：一个永远不应该被破坏的规则。

如果这个不变量被违反，这意味着要么有价值为零的份额，要么无法认领的资金。在 Trident 的合约部署之前，通过 Certora Prover 发现了这一属性的违反，揭示了代码中的一个错误，随后被解决。

神话 3：形式验证必须在代码稳定时进行一次

“程序员的问题在于，你永远无法知道程序员在做什么，直到为时已晚。”

- 西摩·克雷

智能合约是形式验证的理想应用，因为错误代价高昂，且代码通常较小或模块化，并随着时间而演变。形式验证通过在开发和部署过程中找到错误并数学上证明其不存在，来提高智能合约的安全性。

许多 DeFi 项目普遍的看法是，形式验证必须在最后进行，在审核之后以及代码稳定时进行。根据我们的经验，这种做法会导致安全性和生产力降低。

我们认为，最好在流程管道尽可能早安排形式验证，在任何代码冻结之前，甚至在代码功能完成之前。这样的提前方法有多个好处。首先，在编码之前思考并正式声明系统的不变量，有助于明确初始设计中的不足，并指导最终的实施。其次，早期启动形式验证，特别是在使用自动化工具时，可以在代码经过审查过程之前识别难以发现的错误，并快速确认此类错误何时潜入。换句话说，越早发现错误，尤其是通过自动化形式验证发现的困难和棘手的错误，修复就越容易。最后，通过提前启动验证，你可以从一开始就编写为形式验证而设计的代码，而不是在开发后发现整个部分需要昂贵的重写，使其适合形式验证。形式验证工具的长期价值之一在于与 CI/CD 的集成，并在每次代码更改时运行自动检查，以确保不引入错误。这些自动化工具包括像 Certora Prover 这样的机械化验证器或像 Foundry 和 Echidna 这样的模糊测试工具。

形式验证可以与审计同时进行并互为补充。其一大好处是经济的；在人工审核之前提前开始形式验证可以降低成本。此外，审计员可以检查规范，以确保自动工具提供的形式保证与程序员的预期相符。正如已发表的研究反复发现的那样，甚至强大的用户也可能在编写规范时犯许多错误，例如在 时间模型检测中的虚空高效检测 中提到的。

形式验证被越来越多地接受，不仅仅是作为一个有用的工具，而是作为智能合约安全的一个必须品。尽早启动形式验证（并经常使用）对于成功的将其集成到任何项目中至关重要。

神话 4：形式验证必须精确执行，建模确切的机器语义

“抽象与模糊是截然不同的……抽象的目的不是为了模糊，而是创造一个可以绝对精确的新语义层级。”

— 埃德斯格·迪克斯特拉

区块链是极其复杂的分布式系统，其正确性依赖于数千个不可信节点运行复杂软件的协调。对区块链实现的细节进行形式建模在开发时间和计算时间上都是不可承受的，但这并不意味着形式验证不是验证智能合约的有用工具。

相反，智能合约是形式验证的极佳目标，因为区块链提供了抽象接口，具有简单且定义良好的语义。智能合约开发者不需要考虑复杂的细节，例如网络通信或加密原语，因为他们的合约不会（且无法）直接与这些原语交互。相反，智能合约仅限于通过一个具有少量指令和清晰定义的机制与其他合约交互的专用虚拟机所提供的接口。由于系统实现是受信计算基础的一部分，开发者无需思考它。

形式验证工具也不必考虑底层实现的推理。就像合约开发者一样，它们可以将区块链的正确操作作为假设，简单地使用虚拟机提供的抽象语言推理智能合约的行为。通过抽象底层实现的细节，验证工具可以在合理的时间内提供证明，并以智能合约开发者理解的语言给出反例。

事实上，抽象的过程可以进一步扩展：不必使用虚拟机的语义建模智能合约的精确操作，通过证明程序的近似属性通常是足够的。像 Dafny 和 Certora Prover 这样的工具允许用户用一个简单的假设替换计算某个值的复杂程序，这可以大幅降低验证时间。只要被替代的程序片段满足这些假设，对于实际实现的近似证明依然有效。

例如，像取平方根这样的非线性操作对于 SMT 求解器来说可能难以推理（而计算它们的算法更是如此），但是 DeFi 协议的许多重要属性只需使用平方根是一个增函数这一事实即可证明。表示平方根函数实现的逻辑公式远比表示任意增函数的公式大得多；用后者替代前者可以将验证时间从数小时甚至数天缩短到几分钟。

仅仅因为一个系统复杂并不意味着形式验证是不可能的。通过选择正确的抽象层级，形式验证工具可以证明极其复杂系统的重要属性。

神话 5：形式验证产生无懈可击的代码

“我只证明了算法的正确性，并没有对其进行测试。”

― 唐纳德·克努斯

关于形式验证最大的一个误解是，经过形式验证的程序就不可能出错。出于几种原因，代码即使在经过形式证明后仍然可能包含错误。

最常见的原因是规范不充分。规范可能是空洞的，即与代码无关。例如，形式为 x = 5 => x > 0 的不变量是个重言式。与 x 的值无关，这个不变量必须成立。要么 x 等于5，从而大于零；要么它不等于5，从而该论断成立。证明这个不变量并不能对代码提供任何保证，甚至可能让我们对代码的正确性有一种虚假的信心。

人们在写正式规范时可能会犯错。Certora prover 包括简单的空洞检查，报告空洞的不变量。

经过形式验证后的另一个不正确代码的原因是缺失的规范。如果没有编写与该错误相违背的规范，形式验证工具将无法找到错误。规范的编写者应力求涵盖程序尽可能多的区域，优先考虑最关键的部分，以应对失败时可能导致的最糟糕后果。

我们正在实施突变测试，检查正确性规则集是否充分，通过突变程序并检查形式验证是否捕获错误突变。如果错误被遗漏，则规范缺少一些关键属性。

避免计算机错误没有万灵药。形式验证是另一种工具，可以在人工努力和其他机制之上增加代码的安全性。

神话与现实

虽然形式验证领域已经发展了数十年，但在许多软件应用中仍不常用。因此，关于形式验证的许多误解在广泛流传。我们希望这篇文章能让你更好地理解这一新兴技术、其面临的挑战和局限性。我们在 Certora 的使命是让形式验证成为智能合约的标准实践，并提高生态系统的安全性。

• 原文链接： certora.com/blog/5myths...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～