形式化验证介绍

Certora 形式化验证

形式化验证简介

模块1：规则和基本CVL语法

最后更新于2026年2月13日

形式化验证是通过数学方法证明程序符合规范的过程。

本文将概念性地介绍形式化验证的工作原理、它与模糊测试的比较，以及形式化验证的局限性和优势。

“规范”的定义

规范是在特定条件下明确定义的行为。

以下是一些适用于DeFi智能合约的规范示例：

(1) 如果没有时间流逝，贷方不应赚取任何利息。

(2) 如果时间已流逝且存在活跃借款，贷方应赚取超过零的利息。

(3) 如果协议未暂停，借款人可以随时偿还贷款。

(4) 如果未超出供应上限且协议未暂停，贷方可以随时存入资金。

形式化验证还允许我们推理合约的内部状态。我们可以编写如下所示，仅检查存储变量的规范：

(5) 对于任何交易序列，ERC-20 代币的余额总和应等于总供应量。

(6) 如果未调用 deposit()，则 balance 不能增加。

假设我们有一种方法可以确定“(1) 如果没有时间流逝，贷方不应赚取任何利息。”在这种情况下，我们知道通过不应获得的利息从协议中窃取资金的特定攻击向量是不可能的。虽然我们不保证协议没有漏洞，但我们知道它没有特定的漏洞。

考虑如果规范“(2) 如果时间已流逝且存在活跃借款，贷方应赚取超过零的利息”被违反的含义。这意味着有人在借钱，但贷方没有赚取利息。这意味着存在以下情况之一：

• 一个漏洞，协议正在赚取利息，但不是贷方
• 借款人支付的利息流向了不应流向的账户——或者利息被销毁了
• 借款人根本没有支付任何利息

确定规范2成立的好处在于，我们知道上述任何漏洞都不适用于该协议。

如果3和4成立，那么这就消除了所有类别的拒绝服务攻击。如果攻击者有办法阻止借款人偿还，那么他们就可以强迫借款人累积利息，然后以不公平的利润清算借款人。另一方面，如果攻击者可以阻止贷方存款，那么恶意的竞争对手可能会试图通过在第一时间阻止存款来将流动性从该协议中转移走。

如果5和6成立，我们可以确定不存在与ERC-20存储变量会计不匹配相关的漏洞。

形式化验证只能捕获我们为其创建了规范的漏洞。以ERC-20为例，如果我们让 burn(address from, uint256 amount) 函数不受保护（即我们允许任何人调用它——没有访问控制），那么上述任何规范都无法捕获缺失的访问控制。

我们将在本系列中研究的形式化验证工具 Certora Prover，它在字节码级别上推理智能合约。这意味着，如果编译器引入了漏洞，那么形式化验证可以捕获它，只要该漏洞导致违反了我们的一项规范。

作为状态转换声明的规范

使用“ERC-20 代币所有余额的总和应等于总供应量”的规范，形式化验证工具将定义两件事：

1. 状态转换函数 $\phi$
2. 状态的表示（在特定时间点的值集合，例如合约的存储变量和以太坊账户余额），我们简称为 $\texttt{state}$。我们可以将特定状态称为 $\texttt{state}_i$，将不同的状态称为 $\texttt{state}j$。我们也可以将 $\texttt{state}{i+1}$ 称为在 $\texttt{state}_i$ 期间发生交易并导致一些存储变量或账户余额发生变化后的状态。

第一个是状态转换函数 $\phi$，它给定一个状态（例如存储变量和账户余额）、环境（例如区块时间戳）和交易的 calldata，生成一个新的状态：

$$ \texttt{state}_{i+1}=\phi(\texttt{state}_i,\texttt{calldata},\texttt{environment}) $$

这个函数 $\phi$ 是智能合约字节码的数学表示。然后，我们的规范“所有余额的总和等于总供应量”将被编译成以下数学公式：

$$ \forall_i \sum_a \texttt{state}_i.\texttt{balances}_a=\texttt{state}_i.\texttt{total_supply} $$

换句话说，对于任何状态 $i$，在该状态下每个账户 $a$ 的余额总和（$\sum_a \texttt{state}_i.\texttt{balances}_a$）等于该状态的 total_supply。

现在假设我们给定一个状态转换函数 $\phi:\texttt{state}\rightarrow\texttt{state}'$。我们想知道，如果将任何遵守上述公式的 $\texttt{state}$ 代入 $\phi$，那么所得的状态 $\texttt{state}'$ 是否也遵守该公式。（请注意，我们的规范独立于 $\phi$）。

Prover 将尝试通过归纳法（如果这个术语不熟悉也无需担心——我们将在后面的章节中讨论它）来证明，如果 $\texttt{state}_i$ 遵循上述规范，那么之后发生的任何状态也必须遵循该规范。

$\phi$ 本身就是智能合约，因为它接受一个状态、calldata 和一个环境，并产生一个新的状态。我们上面编写的公式是我们希望智能合约具有的属性。

作为一个附带好处，如果存在导致违规的 $\texttt{state}$ 和 $\texttt{calldata}$，Certora Prover 将提供一个示例。

像 Certora Prover 这样的自动化形式化验证工具的巨大好处是，它通过将智能合约的字节码转换为状态变量、calldata 和环境变量的数学函数，为我们推导出了函数 $\phi$。这是一个极其复杂的过程，需要大量的研究和开发，但幸运的是，我们大部分时间都可以将其视为一个黑盒（有一些重要的例外情况，我们将在后面探讨）。

示例规范

我们将“如果没有时间流逝，贷方不应赚取任何利息”的例子用数学表示为：

$$ \forall i,j:\texttt{state}_i.\texttt{timestamp} == \texttt{state}_j.\texttt{timestamp}\rightarrow \texttt{state}_i.\texttt{interestEarned} == \texttt{state}_j.\texttt{interestEarned} $$

这表示“如果状态 $i$ 和 $j$ 的区块时间戳相等，那么 interestEarned 必须相同。”

如果这些数学表达式读起来有点奇怪，请不用担心。我们可以将其翻译为：

• $\forall_{i,j}$ 意味着“对于所有 $i$ 和 $j$”或“对于 $i$ 和 $j$ 的任意两个值”
• $\texttt{state}_i.\texttt{timestamp} == \texttt{state}_j.\texttt{timestamp}\rightarrow$ 如果这两个状态具有相同的时间戳
• $\texttt{state}_i.\texttt{interestEarned} == \texttt{state}_j.\texttt{interestEarned}$ 那么 interestEarned 是相同的

请注意，$\rightarrow$ 在常规编程中表现为“if then”（如果则）。Certora 实际使用的语法更像 Solidity 而不是我们上面所写的数学，但其底层含义是相同的。

形式化验证 vs 模糊测试

形式化验证和模糊测试实现相同目的，但使用不同的策略来达成目标。模糊测试使用随机但通常有引导的交易序列来尝试查找不变量的违规。他们通过运行数千甚至数百万次测试来做到这一点。

另一方面，形式化验证通过数学方法证明不变量成立。

相比之下，模糊测试无法证明没有漏洞。它只能表明在它测试的案例中不存在漏洞。

模糊测试对智能合约进行数千或数百万个随机案例的测试。形式化验证测试所有可能的输入和存储变量值的组合。

形式化验证的局限性

形式化验证本质上是自动编写数学证明——而且它可能非常强大。

例如，计算机已经证明或在证明以下各项中发挥了重要作用（示例取自维基百科关于计算机辅助证明的文章）：

• 任何二维地图都可以用四种颜色着色
• Connect-4 游戏中先手者总是获胜，前提是他们采取最佳走法
• 开普勒猜想成立——如果球体放置在一个盒子中，则堆积球体所占据的体积相对于盒子总体积的最高密度不能超过 $\frac{\pi}{3\sqrt{2}}$。
• 魔方最多可以在20步内解决

如上所示，计算机辅助数学证明可能非常强大，但它们不能解决所有抛给它们的问题（如果可以，数学领域就不会再有未解决的问题了）。

使用形式化验证不需要很多数学知识

即使你一生中从未编写过数学证明，你仍然可以使用 Certora Prover。几乎所有东西都对开发者进行了抽象，开发者可以使用类似于 Solidity 的语言定义规范。

然而，对 Prover 正在做什么有些了解仍然很有帮助。例如，一个人可以在不知道 EVM 如何工作的情况下编写和审计智能合约，但这可能会导致效率低下的代码。同样，在不了解内部机制的情况下为 Certora Prover 编写规范可能会导致生成证明耗时过长。

正如你不会因为成本过高而尝试将 jpeg 存储在 EVM 存储变量中一样，在使用形式化验证时，也有一些你必须自觉避免的陷阱。

以下是形式化验证的一些基本局限性：

1. 停机问题 — 给定一个任意程序，可靠地检测无限循环在数学上是不可能的。

如果我们能检测到无限循环，那么我们就能轻易解决数学中的一个未解问题，孪生质数猜想。孪生质数的例子有 (3,5)、(11,13)、(17,19)——它们的差是2。

这个未解决的问题是这些质数是否存在无限个。如果我们能可靠地检测到无限循环，那么我们就可以编写一个程序，寻找可能的最大孪生质数，然后停机。如果程序永不停机，那么我们就知道存在无限个孪生质数。

2. 密码学 — 给定一个据称是哈希输出的32字节序列，是否存在该哈希的原像？寻找哈希的原像极其困难（实际上不可能）。计算机辅助证明并不能让我们打破它们的硬度。

3. 大型非线性方程组 — 具有大量变量的非线性方程组很难在短时间内解决。这里，“线性”意味着我们所求的变量只被常数相乘或与其他未知变量相加。

如果两个未知变量相乘，或者它们被提高到某个幂次，那么我们就有了一个非线性方程组。如果一个形式化验证工具必须间接解决一个非线性方程组，那么该工具可能会花费过多的时间来寻找解决方案。

本教程系列结构

本教程系列重点关注：

1. 如何为 Certora Prover 编写规范的语法
2. 大量可供你自己使用的模式匹配示例
3. 如何避免规范中的错误
4. 如何形式化验证真实的 DeFi 协议

本系列中的每个部分都建立在前面章节的概念之上。因此，我们建议读者按顺序学习本系列，而不是跳着看。

本文是关于使用 Certora Prover 进行形式化验证系列文章的一部分

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