形式化验证是通过数学证明程序符合规范（specification）的过程。

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

“规范”（specification）的定义

规范是指在特定情况下的明确定义的行为。

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

(1) 如果时间没有流逝，出借人不应获得任何利息。

(2) 如果时间已经流逝，并且存在活跃的借款，出借人获得的利息应大于零。

(3) 如果协议未被暂停，借款人始终可以偿还其贷款。

(4) 如果未超过供应上限且协议未被暂停，出借人始终可以存款。

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

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

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

假设我们有办法确切地知道“(1) 如果时间没有流逝，出借人不应获得任何利息”。在这种情况下，我们就可以知道，通过本不应产生的利息从协议中窃取资金的特定攻击向量是不可能发生的。虽然我们不能保证协议没有漏洞（bug），但我们知道它没有这个特定的漏洞。

思考一下，如果规范“(2) 如果时间已经流逝，并且存在活跃的借款，出借人获得的利息应大于零”被违反，这意味着什么。这意味着有人在借款，但出借人没有获得利息。这表明存在以下情况之一：

• 存在一个漏洞，即协议赚取了利息，而出借人没有赚到
• 借款人支付的利息流向了不该去的账户——或者利息被销毁了
• 借款人没有支付任何利息

能够确切知道规范 2 成立的好处在于，我们知道上述任何漏洞都不存在于该协议中。

如果 3 和 4 成立，那么就能消除整个类别的拒绝服务（denial-of-service）攻击。如果攻击者有办法阻止借款人还款，他们就可以迫使借款人累积利息，然后清算借款人以获取不公平的利润。反过来说，如果攻击者可以阻止出借人存款，那么恶意的竞争对手就可以通过在一开始就阻止存款，来试图将流动性从该协议引开。

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

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

我们将在本系列中学习的形式化验证工具 Certora Prover，是在字节码级别对智能合约进行推理的。这意味着如果编译器引入了漏洞，只要该漏洞导致违反了我们的某个规范，形式化验证就能捕捉到它。

作为状态转换声明的规范

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

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

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

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

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

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

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

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

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

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

规范示例

以我们的“如果时间没有流逝，出借人不应获得任何利息”为例，可以在数学上表达为：

这句话的意思是“如果状态 $i$ 和 $j$ 的区块时间戳相等，那么 interestEarned 必须相同。”

如果觉得这些数学符号读起来有点奇怪，请不要担心。我们可以将其翻译为：

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

请注意，$\rightarrow$ 的作用类似于普通编程中的“if then”。Certora 实际使用的语法看起来更像 Solidity，而不是我们上面的数学公式，但底层含义是相同的。

形式化验证与模糊测试（Fuzzing）

形式化验证和模糊测试旨在实现相同的目的，但使用不同的策略来达到同一个目标。模糊测试使用随机但通常有向导的交易序列，来尝试寻找对不变量的违反情况。它们通过运行数千甚至数百万次测试来做到这一点。

另一方面，形式化验证则在数学上证明这些不变量是成立的。

相比之下，模糊测试无法证明漏洞不存在。它只能表明在它测试过的情况中没有出现漏洞。

模糊测试对智能合约进行数千或数百万种随机情况的测试。形式化验证则测试输入和存储变量值的每一种可能组合。

形式化验证的局限性

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

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

• 任何二维地图都可以用四种颜色着色
• 在四子棋（Connect-4）游戏中，只要采取最优策略，先手玩家必胜
• 开普勒猜想是真的——如果将球体放入一个盒子中，堆积的球体所占据的体积与盒子总体积的最高密度之比不能超过 $\frac{\pi}{3\sqrt{2}}$。
• 魔方（Rubik’s Cube）最多可以在 20 步内还原

从上面可以看出，计算机辅助的数学证明可以极其强大，但它们并不能解决抛给它们的任何问题（如果可以的话，数学界就没有未解之谜了）。

你不需要懂很多数学就能使用形式化验证

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

然而，对 Prover 正在做的事情有一些了解仍然是有帮助的。例如，即使不知道 EVM 是如何工作的，人们也可以编写和审计智能合约，但这可能会导致代码效率低下。同样，如果在不了解底层原理的情况下为 Certora Prover 编写规范，可能会导致生成证明的时间过长。

就像你不会因为高昂的成本而试图将 jpeg 存储在 EVM 存储变量中一样，在使用形式化验证时，也有一些陷阱是你必须有意识地避免的。

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

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

如果我们能够检测出无限循环，那么我们就可以轻松解决数学界的一个未解问题，即孪生素数猜想（twin prime conjecture）。孪生素数的例子有 (3,5)、(11,13)、(17,19) ——它们之间的差值为两。

这个悬而未决的问题在于这些素数是否存在无限多个。如果我们能可靠地检测出无限循环，我们就可以编写一个程序，寻找可能的最大孪生素数，然后停止运行。如果程序永远不停止，那么我们就知道存在无限多个孪生素数。

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

3. 大型非线性方程组（Large non-linear systems of equations） — 包含大量变量的非线性方程组很难在短时间内求解。这里的“线性”意味着我们要解的变量仅仅是乘以常数，或与其他未知变量相加。

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

本系列教程的结构

本系列教程的重点在于：

1. 如何为 Certora Prover 编写规范的语法
2. 提供大量可供你参考并在自身实践中进行模式匹配的示例
3. 如何避免规范中的错误
4. 如何对真实的 DeFi 协议进行形式化验证

本系列的每一部分都建立在前几章概念的基础上。出于这个原因，我们建议读者按顺序学习本系列，而不是跳跃式阅读。

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