为什么形式化验证是DeFi和Web3安全的必需品

Certora
发布于 9小时前
阅读 39

本文强调了形式化验证（FV）在Web3和DeFi安全中的重要性，指出传统测试方法不足以应对Web3的安全挑战。FV通过数学证明确保代码按预期运行，能预防高危漏洞，并已在多个知名DeFi项目中应用，同时建议将FV尽早集成到开发生命周期中，以提升代码质量和安全性。

### 介绍

**唯一**一种能够一次又一次成功保护安全关键型应用的技术是形式化验证¹。DeFi 应用**是**安全关键型的 —— 这些应用中的漏洞可能被利用，造成灾难性的后果，不幸的是，现实世界不乏 демонстрирующий 这一点的事例。因此，形式化验证对 DeFi 的重要性怎么强调都不为过。DeFi 领域的杰出领导者，如 Vitalik Buterin 和 Anatoly Yakovenko，[认识到](https://x.com/VitalikButerin/status/1827681355406147587) [这一点](https://x.com/aeyakovenko/status/1628892536193581057)。形式化验证对于所有 Web3 层都应该是**强制性**的，包括 DeFi 应用、共识协议的实现以及与 DeFi 应用交互的用户界面。

### 什么是形式化验证？

形式化验证（FV）是一种为软件和硬件系统提供安全保证的技术。它补充了诸如测试和模糊测试之类的技术，这些技术只能**有时**基于预定义的属性检测到错误。同样，最佳编码实践和审计可以提高对程序无错误状态的信心，但它们不能提供任何正确性保证，即代码中的某些错误对于所有输入都是不可能的。

相比之下，FV 产生了一个数学证明，证明该程序在**所有**执行过程中都按照规范运行。此外，它可以防止由于硬件和软件系统中的极端情况而导致的罕见错误在生产之前发生。一个经典的 [现实世界的例子](https://en.wikipedia.org/wiki/Pentium_FDIV_bug) 是著名的奔腾硬件，其中硬件电路包含一个非常罕见的错误，该错误通过各种测试机制潜伏下来。事实上，这个错误导致了 FV 方法在硬件行业的广泛采用。

FV 依赖于一个**规范**，该规范正式声明了一个系统必须满足的安全属性。一个好的、可重复使用的规范应该是**通用的**——它应该表达系统的预期行为，而不会过于陷入实现的细节。例如，一个系统可能要求某个用户 Alice 不要双重花费一定数量的 Ether。一个更通用的规范会说，在执行过程中，**任何**用户都不能双重花费**任何**代币。FV 的一个额外好处是，人们在识别和编写所需属性的过程中，可以更好地理解系统。

### 为什么 Web3 需要 FV？我们需要加倍努力吗？

对于大多数软件系统，测试、质量控制、模糊测试（使用随机输入来查找错误）和静态分析就足够了 —— 它们中的大多数在出现罕见错误时表现良好，并且失败通常不会造成严重的后果。运行时监控工具通常也很擅长检测生产中的错误，从而使开发人员可以快速修复问题，而不会造成重大损失。

然而，Web3 与其他领域不同，**在这种情况下，FV 是必不可少的**，原因如下：

1. **低准入门槛 = 易于攻击：** Web3 的美妙之处在于，API、代码和数据对世界各地的每个人都是开放和可访问的。此外，大多数逻辑都体现在小型、可读的程序中，这使得新手可以快速构建 Web3 应用程序。不幸的是，这也使 Web3 成为黑客的完美目标。
2. **小型程序承载着巨大的价值：** 对于 Web3 程序来说，代码行数与价值的比率通常很高。例如，Uniswap V2 包含 424 行代码，并且已经处理了超过 **10740 亿美元**。
3. **巨大的声誉损害：** Web3 应用程序中的罕见错误已经被利用，导致数十亿美元的损失。 这些错误会对协议产生深远的影响，并造成声誉损害。除了对代币价值产生负面影响外，它还可能导致难以吸引用户参与未来的项目。
4. **监控可以被绕过：** 动态监控工具在实时检测事件方面不够快。很多时候，警报在为时已晚时才被看到，并且总是可以被复杂的攻击者绕过，例如，通过私有内存池。
5. **错误缓解是不可能的：** 协议无法在用户不损失资产的情况下减轻错误造成的后果。这对于可变和不可变智能合约都是如此。区块链的公共性质允许攻击者跟踪社交媒体中的消息和代码更改。例如，一位白帽黑客发现 [Balancer V2 中的一个舍入误差](https://rekt.news/balancer-rekt)。该协议负责任地采取行动，要求用户提取他们的资产，但仍损失了数百万美元。

### 形式化验证的优势

1. **通过数学证明保证安全：** FV 通过数学方式证明代码的行为符合预期。相比之下，传统的测试和模糊测试方法只能在所选输入表现出错误时才能发现错误。
2. **防止罕见、高影响的错误：** FV 已被用于检测罕见但高影响的漏洞，这些漏洞已经通过了其他方法。示例包括 [MakerDao 不变量违规](https://learnblockchain.cn/article/13873)，使 **100 亿美元**面临风险，[Balancer V2](https://learnblockchain.cn/article/14768) 资不抵债错误，以及 [Sushi Trident Bug](https://learnblockchain.cn/article/13869)，它可能已被用于耗尽协议。
3. **确保升级后的安全：** 代码升级可能会引入严重的漏洞。[Euler V1](https://rekt.news/euler-rekt) 和 [Ronin Bridge](https://rekt.news/ronin-rekt) 都在看似微小的更改后遭受了九位数的损失。 减轻这种情况的一种方法是将 FV 集成到协议的构建系统中，以确保每次代码修改后的安全性。
4. **加深协议理解：** 编写正式规范的过程迫使团队澄清假设，了解哪些不变量必须成立以及原因，并识别边缘情况，从而带来更好的设计、更简单的代码和精确的文档。
5. **建立超越模糊测试和测试的信誉和信任：** FV 表明了对安全性的承诺，这种承诺超越了复选框审核。领先的协议，如 [Aave](https://www.certora.com/reports/aave-vault), [MakerDAO (Sky)](https://github.com/makerdao/dss-vest/tree/master/certora), [Lido](https://www.certora.com/reports/lido-dual-governance-audit-report), [Jito](https://www.certora.com/reports/jito-tip-router-security-report), [Uniswap](https://www.certora.com/reports/uniswap-v4), [Euler](https://www.certora.com/reports/euler-vault-kit), [Morpho](https://docs.morpho.org/overview/resources/formal-verification/), [Kamino](https://www.certora.com/reports/kamino-lending-security-report), 和 [Solana Token Extension](https://www.certora.com/reports/solana-foundation-security-report) 依靠它不仅来保护他们的代码，而且还将他们定位为“安全第一”方法中的领导者。保险提供商认识到风险降低，并且更有可能提供较低的保费。

### FV 如何融入你的开发生命周期？

开发人员和安全研究人员可以并且**应该**尽早使用 FV，用于 SDLC 中的错误检测，如下图所示。 这不仅会带来更可靠的软件，还会带来更简单的设计，从而更容易扩展和维护。

我们建议将形式化验证集成到 CI 中，就像编译器、模糊器、静态分析器和代码检查器一样。 像 Aave 这样的公司已将形式化验证集成到他们的常规 CI 管道中，每次代码更改后都会调用 [Certora Prover](https://www.certora.com/prover)。 例如，自 2022 年 3 月以来，Aave V3 已将 Certora Prover 集成到其 CI 系统中，并且每次代码更改都会自动检查。

![](https://img.learnblockchain.cn/2025/04/25/80906331_image.png)

### 关于形式化验证的问答

#### 问：在 FV 之后，我的代码是否仍然存在错误？

FV 提供了一个数学证明，证明该程序的行为符合规范，该规范充当“单一的事实来源”。如果规范本身不能准确地编码程序的预期行为，那么 FV 结果就不可信。同样，如果规范没有涵盖某些属性，那么 FV 就无法保证系统不会因为违反该属性而出现错误。

错误也可能由于外部事件而发生，例如定价或对其他未经过形式化验证的库和基础设施代码的依赖。

最后，FV 工具本身可能存在错误。[一些](https://rocq-prover.org/) FV 工具通过最小化必须信任的部分（称为可信计算基础或 TCB）来[降低了这种情况的可能性](https://dl.acm.org/doi/10.1145/3167089)。一些工作已经展示了如何[形式化验证](https://dl.acm.org/doi/pdf/10.1145/3498709) 和 [差异化测试](https://dl.acm.org/doi/abs/10.1145/3533767.3534382) 形式化验证工具本身。

协议可能在 FV 之后被黑客入侵。最可能的原因是缺少规范、对外部事件（如定价）的依赖中的错误，以及在验证范围之外甚至在代码之外的错误。尽管如此，FV 极大地提高了 Web2 和 Web3 中代码的安全性。

#### 问：FV 是否取代审计或模糊测试？

答：不，FV 在许多方面补充了模糊测试和审计。例如，审计规范可以提高对 FV 结果的信心。相反，当 FV 发现违规时，它通常会生成一个触发该错误的具体输入（称为“反例”）。此输入可用作测试用例或模糊器的种子，以使其更有效。最后，[不变性测试](https://book.getfoundry.sh/forge/invariant-testing) 是 FV 的一个良好的起点。

#### 问：可以使用形式化验证测试或证明什么？

对于任何给定的规范，形式化验证都提供**完整的**路径覆盖。例如，规范可能声明只能在 ERC20 合同中铸造有限数量的代币。形式化验证要么保证规则在所有路径和所有输入上都成立，要么生成一个测试输入来演示规则违规。

#### 问：谁可以做 FV？

答：任何对理解协议和代码感到好奇，并且具有编程和逻辑基础知识的人，包括开发人员和安全研究人员。FV 可以提高程序员的技能。

#### 问：应用 FV 的最佳时间是什么时候？

答：应该尽早且经常地使用 FV，最好甚至在编写代码之前的设计阶段就使用。 “FV 思维”会带来更简单、模块化的设计，从而使 FV 更易于应用。

#### 问：FV 是一次性的事情吗？

答：不，FV 应该是系统 CI 的一部分，以便在任何代码更改后运行。

#### 问：如何检查 FV 的质量？

答：FV 结果的质量仅与规范一样好。因此，必须检查规范是否存在诸如空洞性之类的问题。还应使用合成故障注入和 [mutation 测试](https://learnblockchain.cn/article/13835) 以确保规范能够捕获错误。强烈建议审查和审计规范。

### 总结

2023 年 3 月，智能合约中的一个未经检查的错误导致 1.8 亿美元的用户资金被盗。 像这样的事件不是异常现象，它们是社区必须认真对待的警告。 智能合约审计、模糊测试和测试当然有帮助，但它们并不够。

自图灵在 1950 年代首次提出以来，[形式化验证](https://www.certora.com/audits) (FV) 已经取得了长足的进步。 现在有许多强大的 FV 证明工具，包括 SMT 求解器，如 Z3、Yices 和 CVC5，以及交互式定理证明器，如 Lean2、K、Coq 和 Isabelle。

[对于构建 DeFi 协议、治理合约或任何具有经济风险的关键任务应用程序的团队来说，FV 是必不可少的，鉴于存在大量可用于 FV 的优秀工具，根本没有理由不使用它。

##### \[1] 参考文献：

https://dl.acm.org/doi/10.1145/780822.781149

https://link.springer.com/chapter/10.1007/978-3-319-41540-6\_2

https://www.absint.com/astree/index.htm

https://compcert.org/

https://dl.acm.org/doi/10.1145/2737924.2737958

https://sel4.systems/

https://dl.acm.org/doi/10.1145/3051092

https://github.com/starkware-libs/formal-proofs

https://medium.com/nethermind-eth/clear-prove-anything-about-your-solidity-smart-contracts-04c6c7381402

>- 原文链接： [certora.com/blog/formal-...](https://www.certora.com/blog/formal-verification)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

介绍

唯一一种能够一次又一次成功保护安全关键型应用的技术是形式化验证¹。DeFi 应用是安全关键型的 —— 这些应用中的漏洞可能被利用，造成灾难性的后果，不幸的是，现实世界不乏 демонстрирующий 这一点的事例。因此，形式化验证对 DeFi 的重要性怎么强调都不为过。DeFi 领域的杰出领导者，如 Vitalik Buterin 和 Anatoly Yakovenko，认识到这一点。形式化验证对于所有 Web3 层都应该是强制性的，包括 DeFi 应用、共识协议的实现以及与 DeFi 应用交互的用户界面。

什么是形式化验证？

形式化验证（FV）是一种为软件和硬件系统提供安全保证的技术。它补充了诸如测试和模糊测试之类的技术，这些技术只能有时基于预定义的属性检测到错误。同样，最佳编码实践和审计可以提高对程序无错误状态的信心，但它们不能提供任何正确性保证，即代码中的某些错误对于所有输入都是不可能的。

相比之下，FV 产生了一个数学证明，证明该程序在所有执行过程中都按照规范运行。此外，它可以防止由于硬件和软件系统中的极端情况而导致的罕见错误在生产之前发生。一个经典的现实世界的例子是著名的奔腾硬件，其中硬件电路包含一个非常罕见的错误，该错误通过各种测试机制潜伏下来。事实上，这个错误导致了 FV 方法在硬件行业的广泛采用。

FV 依赖于一个规范，该规范正式声明了一个系统必须满足的安全属性。一个好的、可重复使用的规范应该是通用的——它应该表达系统的预期行为，而不会过于陷入实现的细节。例如，一个系统可能要求某个用户 Alice 不要双重花费一定数量的 Ether。一个更通用的规范会说，在执行过程中，任何用户都不能双重花费任何代币。FV 的一个额外好处是，人们在识别和编写所需属性的过程中，可以更好地理解系统。

为什么 Web3 需要 FV？我们需要加倍努力吗？

然而，Web3 与其他领域不同，在这种情况下，FV 是必不可少的，原因如下：

低准入门槛 = 易于攻击： Web3 的美妙之处在于，API、代码和数据对世界各地的每个人都是开放和可访问的。此外，大多数逻辑都体现在小型、可读的程序中，这使得新手可以快速构建 Web3 应用程序。不幸的是，这也使 Web3 成为黑客的完美目标。
小型程序承载着巨大的价值： 对于 Web3 程序来说，代码行数与价值的比率通常很高。例如，Uniswap V2 包含 424 行代码，并且已经处理了超过 10740 亿美元。
巨大的声誉损害： Web3 应用程序中的罕见错误已经被利用，导致数十亿美元的损失。这些错误会对协议产生深远的影响，并造成声誉损害。除了对代币价值产生负面影响外，它还可能导致难以吸引用户参与未来的项目。
监控可以被绕过： 动态监控工具在实时检测事件方面不够快。很多时候，警报在为时已晚时才被看到，并且总是可以被复杂的攻击者绕过，例如，通过私有内存池。
错误缓解是不可能的： 协议无法在用户不损失资产的情况下减轻错误造成的后果。这对于可变和不可变智能合约都是如此。区块链的公共性质允许攻击者跟踪社交媒体中的消息和代码更改。例如，一位白帽黑客发现 Balancer V2 中的一个舍入误差。该协议负责任地采取行动，要求用户提取他们的资产，但仍损失了数百万美元。

形式化验证的优势

通过数学证明保证安全： FV 通过数学方式证明代码的行为符合预期。相比之下，传统的测试和模糊测试方法只能在所选输入表现出错误时才能发现错误。
防止罕见、高影响的错误： FV 已被用于检测罕见但高影响的漏洞，这些漏洞已经通过了其他方法。示例包括 MakerDao 不变量违规，使 100 亿美元面临风险，Balancer V2 资不抵债错误，以及 Sushi Trident Bug，它可能已被用于耗尽协议。
确保升级后的安全： 代码升级可能会引入严重的漏洞。Euler V1 和 Ronin Bridge 都在看似微小的更改后遭受了九位数的损失。减轻这种情况的一种方法是将 FV 集成到协议的构建系统中，以确保每次代码修改后的安全性。
加深协议理解： 编写正式规范的过程迫使团队澄清假设，了解哪些不变量必须成立以及原因，并识别边缘情况，从而带来更好的设计、更简单的代码和精确的文档。
建立超越模糊测试和测试的信誉和信任： FV 表明了对安全性的承诺，这种承诺超越了复选框审核。领先的协议，如 Aave, MakerDAO (Sky), Lido, Jito, Uniswap, Euler, Morpho, Kamino, 和 Solana Token Extension 依靠它不仅来保护他们的代码，而且还将他们定位为“安全第一”方法中的领导者。保险提供商认识到风险降低，并且更有可能提供较低的保费。

FV 如何融入你的开发生命周期？

开发人员和安全研究人员可以并且应该尽早使用 FV，用于 SDLC 中的错误检测，如下图所示。这不仅会带来更可靠的软件，还会带来更简单的设计，从而更容易扩展和维护。

我们建议将形式化验证集成到 CI 中，就像编译器、模糊器、静态分析器和代码检查器一样。像 Aave 这样的公司已将形式化验证集成到他们的常规 CI 管道中，每次代码更改后都会调用 Certora Prover。例如，自 2022 年 3 月以来，Aave V3 已将 Certora Prover 集成到其 CI 系统中，并且每次代码更改都会自动检查。