形式化验证最受欢迎的智能合约 WETH

摘要

Wrapped ETH 或 WETH↗ 是以太坊最流行的智能合约之一。虽然 WETH 的用途很简单，但所有以太坊交易中有很大一部分依赖于它。WETH 目前支撑着 DeFi 的大部分部分。在这篇博客中，我们证明了 WETH 合约中的关键安全保证和不变式。我们通过利用 Z3，这个经过测试的 SMT 求解器来实现这一点。

我们证明了两个关键的不变式：（1）账目准确性和（2）偿付能力。在账目方面，我们证明了 WETH 的总供应量始终等于其原生以太的余额。在偿付能力方面，我们证明了无论其他用户的行为如何，用户始终能够解除 Wrapped ETH 的抵押。在此过程中，我们还发现了合约中的一个小的、无害的漏洞。我们的工作使社区能够以更高的信心继续使用 WETH。

背景

WETH 是一个简单的代币，将原生以太包装成 ERC20 兼容的 WETH 代币。该合约允许任何人 1:1 存入原生以太以换取 WETH 代币，反之亦然，也可以将 WETH 兑换为原生以太。该合约还支持标准 ERC20 功能，如批准、转账、总供应量和转移。

WETH 是有用的，因为原生以太在智能合约中使用不方便。首先，原生以太不兼容 ERC20。这需要额外的代码路径，增加了复杂性。不仅增加了开发负担，还加大了安全漏洞的可能性。与原生以太的交互也引入了重入漏洞的风险，而与 ERC20 代币的交互则不存在这种风险。因此，WETH 在 DeFi 应用程序中得到了广泛应用，比如 Uniswap、Compound 等。

截至撰写时，WETH 已经涉及超过 1.25 亿笔交易1。在整个以太坊区块链上，到目前为止，总交易量为 17 亿笔。换句话说，超过 7% 的所有以太坊交易 涉及 Wrapped ETH。此外，随着时间的推移，Wrapped ETH 变得越来越普遍。在过去的一年中，有 4800 万笔以太坊交易涉及 WETH。这代表了今年所有以太坊交易的 11.5%。由于 WETH 在 DeFi 应用程序中被广泛使用，而 DeFi 又成为 Web3 生态系统的核心，因此这是一种自然的结果。

WETH 中的智能合约漏洞将是致命的。无数 DeFi 协议使用 WETH 作为原生 ETH 的兼容层。例如，Uniswap 在处理原生 ETH 时依赖 WETH↗。如果 WETH 存在偿付能力或账目错误，DeFi 的下游影响将是巨大的。WETH 持有者不仅会受到影响，所有硬编码使用 WETH 的 DeFi 协议也会受到影响。

WETH 合约本身相对简单。排除空行和注释，WETH9 总共仅由 51 行代码组成。排除获取函数，只有 7 个函数，每个函数相对简单。尽管如此，简单性并不能保证正确性。事实上，首次已知的重入攻击实例就是在一个 WETH 风格的封装合约上执行的↗。此类事件突显了对关键智能合约进行正式验证的重要性。

话虽如此，让我们迅速回顾 WETH 中最重要的函数：

• balanceOf：从地址到 uint256 的映射，用于跟踪给定地址“拥有”的 WETH 数量。
• deposit：可支付函数。接受 msg.value 中的原生 ETH 并通过增加其在 balanceOf 中的账户条目为 msg.sender 铸造新的 WETH。
• withdraw：函数。通过从发件人的 balanceOf 中减去生成 WETH，并分发相同数量的原生 ETH。
• totalSupply：查看函数。通过获取 WETH 合约本身所存的原生 ETH 余额来计算所发行的 WETH 的总量。
• transferFrom：函数。在不同账户之间转移 WETH 代币。它还强制执行 ERC20 代币的允许规则，阻止未授权的转账。

在我们验证 WETH 的正确性时，需要牢记这些函数。

方法

使用 Z3Py，我们在 SMT 方程中重新实现了 WETH 合约的行为。然后我们使用 Z3 定理证明器来证明关于符号化的 WETH 合约的某些事实。首先，我们证明涉及 WETH 内部账目准确性的关键不变式。其次，我们证明了一个不变式，保证 WETH 持有者始终可以提取它们锁定的 ETH。

不变式 1：内部账目准确性

WETH 的一个关键不变式是 totalSupply 必须等于 balanceOf 中所有条目的总和。换句话说，WETH 必须准确跟踪其总供应量。根据 ERC-20 标准，这一点得到了强化。根据 EIP-20，代币的 totalSupply 函数必须“返回总代币供应量”。对像 WETH 这样广泛使用的合约遵守 ERC20 代币标准似乎很重要。

WETH 合同通过简单使用 address(this).balance 来计算 totalSupply，该方法返回合约中存储的原生 ETH 总量。这个数量应该与 WETH ERC20 代币的总供应量相符，因为 balanceOf 和原生 ETH 始终是成比例地相加和相减（分别在 deposit 和 withdraw 函数中）。

有趣的是，在我正式验证这一属性时，我发现这个不变式实际上并不成立↗。有可能导致 WETH 返回一个与所有 WETH 代币总数不相等的 totalSupply。所以严格来说，WETH 的 totalSupply 函数是错误的！但稍后我们将看到为什么这并不重要。

让我们首先开始正式化与这个不变式相关的 WETH 的各个性质。首先，不变式仅依赖于 totalSupply、balanceOf 和合约的原生 ETH 余额。为了这一不变式的目的，我们可以在一个二元组中总结相关的全局状态：（balanceO ⁣f，weth_balance）。这里，balanceO ⁣fbalanceOf 是一个从 address 到 uint256 的映射，而 weth_balance 是一个 uint256。

接下来，由于 WETH 合约可能无法在存在无限流通的原生 ETH 情况下正常运作，我们用第三个变量 eth_supply（uint256）增加我们状态的元组，这个变量表示（上界估算）我们 WETH 合约外的原生 ETH 的总供应量（以 wei 表示）。新变量 eth_supply 将约束交易中的任何原生 ETH 值。因此，我们的状态元组是 (balanceO ⁣f，weth_balance，eth_supply)。

由于这个不变式完全由我们的状态元组参数化，我们只需要考虑状态元组各个组成部分可能受到影响的方式。列举它们，我们有：

• deposit、fallback 和 withdraw：更新 balanceO ⁣f 和原生 ETH 余额
• transferFrom：更新 balanceO
• SELFDESTRUCT 或块奖励 coinbase↗：更新原生 ETH 余额（适用于任何地址，不仅限于 WETH）

我们可以将这些状态过渡形式化为受限的过渡规则。每个规则的形式为 (state,parameters)∣condition⟶new_state，其中 state 和 new_state 是状态元组，parameters 是过渡的参数元组，condition 是过渡有效所需的前提。我们有以下规则：

• deposit: ((balanceO ⁣f,weth_balance,eth_supply),(msg_sender,msg_value))∣msg_value≤eth_supply⟶(Store(balanceO ⁣f,src,balanceO ⁣f[src]+msg_value),weth_balance+msg_value,eth_supply−msg_value)

• withdraw: ((balanceO ⁣f,weth_balance,eth_supply),(msg_sender,wad))∣wad≤balanceO ⁣f[msg_sender]⟶(Store(balanceO ⁣f,msg_sender,balanceO ⁣f[msg_sender]−wad),weth_balance−wad,eth_supply+wad)

• transferFrom: ((balanceO ⁣f,weth_balance,eth_supply),(src,dst,wad))∣wad≤balanceO ⁣f[src]⟶(Store(x,dst,x[dst]+wad),weth_balance),where x=Store(balanceO ⁣f,src,balanceO ⁣f[src]−wad,eth_supply)

• selfdestruct: ((balanceO ⁣f,weth_balance,eth_supply),(value))∣msg_value≤eth_supply⟶(balanceO ⁣f,weth_balance+value,eth_supply−value)

• fallback：与 deposit 相同

• coinbase：与 fallback 基本相同（上界估算）

其中 Store(M,K,V) 表示一个与 M 相同的映射，但 M[A] 被设置为 V。

我们还会为合约定义一个初始状态：

• (K(0),0,120000000e18)，其中 K(0) 表示所有条目初始化为 0 的映射。

我们选择 120000000e18 作为此处 eth_supply 的具体值，因为流通中的以太约为 1.2 亿。由于总 ETH 供应量的很大一部分已经被锁定，这也是一个合理的上界估算。

受限霍恩子句

由于我们的不变式是 归纳 属性，所以像 Z3 这样的 SMT 求解器直接证明起来比较棘手。我们将通过将合约的语义表述为受限的 霍恩子句↗（简写为 CHC）来解决这个问题。方便的是，Z3 拥有相对强大的 CHC 引擎。CHC 也被 solc 的 SMTchecker↗ 使用。然而，我无法使 SMTchecker 内置的 CHC 引擎对我们的用途正常工作。 这可能是由于 Z3 证明器中的限制，这会在文章后面讨论。相反，我们直接使用 Z3 和自己手动编写的 CHC。

尽管有关受限霍恩子句的文献已经存在大量，但为了便于理解，我们将在本节中简单介绍它们。在每个步骤中，我们还将举几个例子来保持友好。

首先，我们定义一个函数，State(s)，当且仅当 s 是一个有效的状态元组，并且可以通过使用我们预定义的一组状态过渡规则从起始状态到达时为真。换句话说，State(s) 列举了我们的智能合约可能到达的所有状态。

例如，State(K(0),0,0) 应该为假，因为所有未清的 ETH 供应量不可能消失；它要么进入 WETH 合约，要么保持流通状态。更形式地说，给定一些 s=(balanceO ⁣f,weth_balance,eth_supply)，则 State(balanceO ⁣f,weth_balance,eth_supply) 必然意味着 weth_balance+eth_supply 始终等于某个常数。在进行正式验证时，我们希望在我们的预定义状态转换和初始状态之外假设尽可能少的东西。要证明这个属性，我们可以将这个蕴含式作为附加断言添加到 SMT 求解器中。

请记住，我们的目标是验证 balanceO ⁣f（实际总供应量）中的所有条目的总和等于 weth_balance（计算的总供应量）。我们将此不变式表述为以下 CHC 断言：

∀s=(balanceO ⁣f,weth_balance,eth_supply): State(balanceO ⁣f,weth_balance,eth_supply)⟹∑abalanceO ⁣f[a]=weth_balance

如果存在一个状态使得该约束不成立，则我们的蕴含断言会被违反。因此， SMT 求解器将报告我们的约束为不可满足。换句话说，求解器报告说，存在一个函数 State，使得它同时遵从我们的状态过渡（即可达性）规则以及我们试图证明的附加约束，需要合成这个函数是不可行的。此外，我们可以查询求证明器给出不可满足的 证明，它提供了从我们起始假设集合到违反状态的一系列逻辑序列。这个序列通常是从我们的初始状态，通过一系列状态转变，到一个非法状态。这对于调试 为什么 我们的假设或不变式无效是非常有帮助的。

另一方面，如果我们的不变式在所有可达状态中成立，那么我们的断言将成立。 SMT 求解器将报告系统为 可满足。换句话说，可以合成与我们的状态过渡规则和不变式一致的函数 State。这也意味着我们的不变式与状态过渡规则是一致的。在这种情况下，我们可以查询求解器以获取一个 模型，该模型实际定义了一个可能的 State 合成的具体定义。这个定义将基本上是一条概述所有可达状态的谓词。

WETH 状态转换规则的 CHC 表述

我们开始声明确一组有效的初始“起始”状态和约束 State(s) 的转换规则。对于 WETH，这基本上是构造函数返回后的合约状态。

State(K(0),0,120000000e18)=True

然后，对于每个转换规则，我们将其表述为一个 CHC 并作出断言。更具体地说，我们的每个公式的形式如下：

∀(s,p):(State(s)∧Pre(p))⟹State(Post(s,p))

其中 s 是状态元组，p 是参数元组，Pre(p) 是一个布尔函数，表示参数 p 的前提条件，Post(s,p) 表示过渡后的更新状态。直观上，这意味着：“对于每个状态 s 和参数向量 p，如果 s 是一个可达状态，并且 p 是有效参数，则我们还可以到达更新状态 Post(s,p)”。

例如，以下是我们针对 withdraw 转换的公式：

∀(balanceO ⁣f,weth_balance,msg_sender,wad): (State(balanceO ⁣f,weth_balance,eth_supply)∧(wad≤balanceO ⁣f[msg_sender]))⟹State(Store(balanceO ⁣f,msg_sender,balanceO ⁣f[msg_sender]−wad),weth_balance−wad,eth_supply+wad)。

此处，前提检查用户是否具有足够的 WETH 余额（由智能合约强制执行），并且 WETH 合约具有足够的原生 ETH 可发送（由 EVM 强制执行）。更新状态与输入状态相同，用户的余额已更新，WETH 合约中的原生 ETH 减少，用户拥有更多原生 ETH。

对数组求和的编码

我们希望检查的不变式是，balanceO ⁣f 中所有值的总和等于 weth_balance；即 ∑balanceO ⁣f=weth_balance。在 SMT 中编码这个总和很困难，因为在标准的 SMT 数组理论中没有自然表达和的方式。

为了解决这个问题，我们引入一个额外的“综合”变量 sum_balanceO ⁣f，跟踪这个总和的值；即 sum_balanceO ⁣f:=∑balanceO ⁣f。我们用这个额外的综合变量增加状态元组。这一技巧是正确的，只要我们相应地更新 sum_balanceO ⁣f 在每次更新 balanceO ⁣f 时。例如，在向 balanceO ⁣f 的任何元素添加或减去时，我们将相应地添加或减去 sum_balanceO ⁣f。

作为 CHC，我们的不变式可以表述为：

∀(balanceO ⁣f,weth_balance,msg_sender,wad,sum_totalSupply): (State(balanceO ⁣f,weth_balance,eth_supply,sum_totalSupply))⟹sum_totalSupply=weth_balance

但是，单独这一修复并不足以在及时的方式上“增强” Z3 的数组理论实现以证明我们的约束系统。作为实施细节，由于 Z3 不“理解” sum_balanceO ⁣f 是 balanceO ⁣f 的总和，它无法轻松证明关于 balanceO ⁣f 中值的全局属性。若被迫，它通常会诉诸于列举所有可能地址的暴力证明。显然，这对于以太坊来说是不可行的（地址是 160 位）。因此，我们还用额外的前提增强所有转换规则，前提是 balanceO ⁣f[x]≤sum_balanceO ⁣f，当过渡使用某个值 balanceO ⁣f[x] 时。这一近似是合理的，因为从定义上讲，sum_balanceO ⁣f 是 balanceO ⁣f 中所有值的总和，总和始终大于或等于单个成分。最重要的是，这些额外的约束使求解器能够更快完成。它能轻易排除那些涉及个别条目的可达状态。

此外，为了帮助求解器更快地完成，我们通过提示求解器证明额外的引理来“指导”它。该引理断言 sum_balanceO ⁣f 和 balanceO ⁣f 中的所有值都必须小于我们总的 eth 供应 120000000e18：

∀(balanceO ⁣f,weth_balance,msg_sender,wad,sum_totalSupply,address): (State(balanceO ⁣f,weth_balance,eth_supply,sum_totalSupply))∧(balanceO ⁣f[address]≤sum_balanceO ⁣f)⟹(sum_balanceO ⁣f≤120000000e18)∧(balanceO ⁣f[address]≤12000000e18)

在我们的实验中，我们发现这个引理对于 Z3 避免暴力证明是必需的。

结果

令人惊讶的是，当我们运行我们的 Z3Py 代码时，立刻发现我们的不变式的反例：

unsat
mp(hyper-res( # "3"
    asserted(ForAll([A, B, C, D], Implies(
        And(
            state(A, B, C, D),
            Not(D == B)
        ), query!1
    ))),
    hyper-res( # "2"
        asserted(ForAll([A, B, C, D, E, F, G], Implies(
            And(
                state(C, D, E, F),
                B == D + G,
                ULE(G, E),
                A == E + 115792089237316195423570985008687907853269984665640564039457584007913129639935*G # 注意：这个大常数是 2^256-1
            ),
            state(C, B, A, F)
        ))),
        hyper-res( # "1"
            asserted(state(K(BitVec(160), 0), 0, 120000000000000002281701376, 0)),
            state(K(BitVec(160), 0), 0, 120000000000000002281701376, 0)
        ),
        state(K(BitVec(160), 0), 12884901888, 119999999999999989396799488, 0)
    ),
    query!1
),
asserted(Implies(query!1, False)),
False)

为了解释这一点，我们从内往外阅读。用通俗易懂的话说，这是在说：

1. 假设的起始状态 (K(BitVec(160),0),0,120000000e18,0) 是可达的。因此，它是可达的。（注意：这里的 hyper-res 被标记为“1”）
2. 你已声明，如果状态可达，我也可以对 WETH 合约进行 SELFDESTRUCT 以达到一个新状态。因此，状态 (K(0),12884901888,119999999e18,0) 是可达的。
3. 你已声明，如果状态可达，则 weth_balance 必须等于 sum_balanceO ⁣f。 但我们知道，状态为 weth_balance = 12884901888 和 sum_balanceO ⁣f = 0 是可达的。
4. 这是一个矛盾，因此你要求我的逻辑上是一致的。这个状态是不满足的。

正如我们之前提到的，这实际上是 WETH 中的一个漏洞（尽管是小漏洞）！totalSupply 可能并不实际是存在的总 WETH 代币数量！这是因为，如 Z3 的证明所示，你可以向 WETH 合约 SELFDESTRUCT。这增加了合约的 ETH 余额，但没有铸造任何新代币。这使得 totalSupply 变量不一致！这是一个常见的漏洞模式↗，以前也有文档记录过，但如此受欢迎的智能合约竟然有这样的漏洞，令人惊讶。这可能是出于预期的 gas 优化，或者是 WETH 开发者认为这个问题无关紧要。

无论如何，我们仍然可以证明另一个同样有价值的 WETH 不变式：WETH 代币的总数始终 小于或等于 WETH 的原生 ETH 余额。请注意，我们在这里放松了约束，从最初的 严格等于 的约束变为 小于或等于 的约束。我们新的 CHC 不变式表述为：

∀(balanceO ⁣f,weth_balance,msg_sender,wad,sum_totalSupply):(State(balanceO ⁣f,weth_balance,eth_supply,sum_totalSupply))⟹sum_totalSupply≤weth_balance

重新运行我们的 Z3Py 代码，我们获得了期望的 sat 结果！

sat
[state = [else ->\
          And(Var(1) == 120000000000000002281701376 + 115792089237316195423570985008687907853269984665640564039457584007913129639935*Var(2),\
              ULE(Var(3), Var(1)),\
              Extract(255, 87, Var(2)) == 0,\
              ULE(154742504910672534362390527*Extract(86, 0, Var(3)) + Extract(86, 0, Var(1)), 120000000000000002281701376),\
              Extract(255, 87, Var(1)) == 0\
          )\
]]

不变式 2：偿付能力

在上一节中，我们证明了 WETH 代币的总数始终小于 WETH 合约的 ETH 余额。然而，这并不一定证明 WETH 持有者实际可以提取他们的 ETH。在这一节中，我们进一步证明 WETH 是 有偿付能力的 ，这意味着 WETH 持有者始终能够在存款后提取其原生 ETH。换句话说，我们表明无论 WETH 合约在存入和提取之间发生了什么，存款者始终能够提取其 ETH。虽然我们可以通过扩展我们的 CHC 公式来证明这个不变式，但这个公式并不太适合 WETH 合约代码中的逐行条件、语句和控制流。例如，我们的 CHC 公式只是描述了状态转移中的前提条件，而没有关注这些前提条件的检查顺序。通常这没问题，因为以太坊交易是原子的，但它突显了我们 CHC 公式是 WETH 合约代码完整语义的简化这一一般问题。

此外，CHC 公式并未对 approve 函数或 transferFrom 中的任何 ERC20 授权功能进行建模。这在之前是可以的，因为我们只关注证明 WETH 状态的一个特定属性。然而，为了对偿付能力（即存款后提取的能力）进行严格保证，我们需要更细致的方法，更精确地建模 WETH 合约代码的语义。更具体地，我们将采用 基于符号执行的方法。

Solidity 的符号执行

解释我们的方法的最佳方式是通过一个例子。让我们以 WETH 函数 approve 为例。下面是该函数的 Solidity 代码：

function approve(address guy, uint wad) public returns (bool) {
    allowance[msg.sender][guy] = wad; // 1
    Approval(msg.sender, guy, wad);   // 2
    return true;                      // 3
}

我们将这个 Solidity 函数翻译成 Z3Py 函数。该函数接收一个状态元组作为输入，如上一节所描述。然后，它将符号执行每个语句。最后，它返回一个更新的状态元组。以下是我们的翻译代码：

def approve(s, state, msg_sender, guy, wad):
    eth_balances, balanceOf, allowance = state

    # allowance[msg.sender][guy] = wad; (1)
    allowance = Store(allowance, msg_sender, Store(allowance[msg_sender], guy, wad))

    # Approval(msg.sender, guy, wad);   (2)

    # return true;                      (3)

    return (eth_balances, balanceOf, allowance)

我们将语句 (1) 符号执行为两个符号存储。在这里，allowance 被符号化为一个从地址到地址数组到 uint256 的 SMT 数组。

我们忽略语句 (2) 和 (3)，因为我们正在建模对 WETH 合约的外部调用。由于日志和返回值不会影响 WETH 的状态，因此我们不关心它们。它们本质上是不会影响 WETH 偿付能力的副作用。

为了获得更深入的示例，让我们看一下 deposit 函数。以下是 Solidity 代码：

function deposit() public payable {
    balanceOf[msg.sender] += msg.value; // 1
    Deposit(msg.sender, msg.value);     // 2
}

以下是对应的符号实现：

def deposit(s, state, msg_sender, msg_value):
    eth_balances, balanceOf, allowance = state

    # 根据 msg_value 转移原生 eth
    s.add(UGE(eth_balances[msg_sender], msg_value)) # 注意：UGE 意思是“无符号大于”
    eth_balances = Store(eth_balances, msg_sender, eth_balances[msg_sender] - msg_value)
    eth_balances = Store(eth_balances, WETH_Address, eth_balances[WETH_Address] + msg_value)

    # balanceOf[msg.sender] += msg.value; (1)
    balanceOf = Store(balanceOf, msg_sender, balanceOf[msg_sender] + msg_value)

    # Deposit(msg.sender, msg.value);     (2)

    return (eth_balances, balanceOf, allowance)

首先，由于 deposit 是一个可支付的函数，我们必须在 msg_value 中建模将原生 eth 转入该函数的操作。我们施加约束，要求发送方的余额必须足以支付 msg_value。这三条 Z3Py 语句是通过 EVM 规则隐含的。

接下来，我们符号执行第 (1) 行，更新 balanceOf。最后，我们可以忽略第 (2) 行，因为它只是发出一个事件，我们不关心它。

最后，让我们看看如何处理 transferFrom 函数中的分支控制流。以下是 Solidity 代码：

function transferFrom(address src, address dst, uint wad)
    public
    returns (bool)
{
    require(balanceOf[src] >= wad);                   // (1)

    if (src != msg.sender && allowance[src][msg.sender] != uint(-1)) { // (2)
        require(allowance[src][msg.sender] >= wad);   // (3)
        allowance[src][msg.sender] -= wad;            // (4)
    }

    balanceOf[src] -= wad;                            // (5)
    balanceOf[dst] += wad;                            // (6)

    Transfer(src, dst, wad);

    return true;
}

以下是我们符号执行的方式：

def transferFrom(s, state, msg_sender, src, dst, wad):
    eth_balances, balanceOf, allowance = state

    # (1)
    s.add(UGE(balanceOf[src], wad))

    # (2)
    p = And(src != msg_sender, allowance[src][msg_sender] != Uint(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))

    # (3)
    s.add(Implies(p, UGE(allowance[src][msg_sender], wad)))

    # (4)
    allowance = If(p,
        Store(allowance, src, Store(allowance[src], msg_sender, allowance[src][msg_sender] - wad)),
        allowance)

    # (5)
    balanceOf = Store(balanceOf, src, balanceOf[src]-wad)

    # (6)
    balanceOf = Store(balanceOf, dst, balanceOf[dst]+wad)

    return (eth_balances, balanceOf, allowance)

当我们以这种方式符号执行代码时，我们实际上必须符号化所有分支的两个路径上的变量值。在语句 (4) 中，若分支被接受，allowance 将获得更新的值（p 为真），否则保持不变（p 为假）。

需要注意的是，在存在循环的情况下，这种符号执行风格可能会导致所谓的 路径爆炸问题↗，每次循环迭代都创建一个额外的 If-else 术语。如果循环是无限的，那么理论上公式的复杂度是无限的。幸运的是，在以太坊智能合约中，循环通常是有界的（例如，由于Gas限制）。因此，循环可以通过“展开”来在符号执行器中处理。这种技术属于一种称为 有界模型检查↗（BMC）的模型检查方法家族。这种界定是一种低估。SMTchecker 支持 BMC，但在撰写本文时不支持展开循环，这是一个弱点（在我看来）。

最后，请注意我们没有对任何 view 函数进行建模。我们在这里并不真正关注它们，因为 view 函数无法影响合约状态。因此，对 view 函数的调用永远不会导致 WETH 变得无偿付能力。

证明偿付能力

我们应用归纳原理来证明偿付能力。从简而言之，我们对偿付能力的论证形式为：

• 基础情况：首先，证明存在 某个 状态是有偿付能力的。
• 归纳情况：给定一个 任意 有偿付能力的起始状态（归纳假设），证明在对 WETH 进行 任意 单笔交易后状态仍然是有偿付能力的。

对此论证的一个可能初步反应可以是：“好的，你证明了它在 一笔 交易后保持了偿付能力。但是涉及 两笔或更多 交易的攻击怎么办？”

这个反论证并不有效，因为在我们的归纳情况下，起始状态是 任何任意 的有偿付能力状态。考虑一个假设的“两笔交易”攻击。显然，该攻击在 第一次 交易后不会导致 WETH 变得无偿付能力，否则该攻击就只是一次交易中的攻击。但由于第一次交易后的状态是有偿付能力的，我们对归纳情况的证明排除了某些交易突然使 WETH 变得无偿付能力的可能性。这样，这种攻击中的假设第二笔交易就不存在。这一论证也适用于三笔交易等攻击。

然而，这个反论证确实表明，我们在归纳情况下 不应对任意起始状态做出任何多余的假设或主张 是至关重要的。

基础情况

基础情况是显而易见的。我们从 WETH 的初始状态（空状态）开始，存入一些资金。显然，我们仍然可以取出这些资金。我们可以通过简单的单元测试证明这一点。为了证明这对 所有 用户地址都是有效的，我们可以使用符号执行。

归纳情况

我们通过简单使用不受约束的变量来建模一个 任意 起始状态。例如，balanceOf 只是一个从地址映射到 uint256 的不受约束的 SMT 数组。我们还将一个特定的、任意的用户及其初始存款（我们将证明其始终保持偿付能力）建模为一个不受约束的地址和 uint256。最后，我们还要建模一个 任意 全局 EVM 状态。出于我们的目的，我们只需要建模一个全局的原生 eth 账户余额映射。

balanceOf = Array('balanceOf', AddressSort, UintSort)
allowance = Array('allowance', AddressSort, ArraySort(AddressSort, UintSort))

myUser = Const('myUser', AddressSort)
initialDeposit = Const('initialDeposit', UintSort)

eth_balances = Array('eth_balances', AddressSort, UintSort)

为了防止求解器生成“无意义”的反例（即那些显然是不可能的，因为它们无法在不违反 EVM 规则或基本数学原理的情况下实现），我们对我们的不受约束状态施加以下假设：

• myUser != WETH_Address：用户不是 WETH 合约本身。
• ForAll([a], ULE(eth_balances[a], 120000000e18))：没有以太坊地址的 eth 超过总供应量。

与我们的 CHC 模型一样，我们需要通过提供一些额外的关于数组之和的定理来“帮助” Z3。首先，数组中的一个条目永远不能超过所有条目的总和。第二，我们已经通过我们的 CHC 模型证明了 balanceOf 中所有条目的总和小于或等于 WETH 的总 eth 余额。因此，balanceOf 中的所有条目都小于 WETH 的余额：

• ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))

请注意，由于该主张，我们对第二个不变式的模型依赖于我们在第一个不变式中所证明的属性。这一主张对于指导 Z3 避免进行不切实际的全力证明是极其重要的。

我们还声明了一些规则以设置我们的假设存款人：

• balanceOf = Store(balanceOf, myUser, Uint(0))：该用户在存款之前没有任何 WETH。（这是可以的，因为我们可以通过简单地提取所有 WETH 来随时回到这个“已知安全状态”）
• ForAll([a], allowance[myUser][a] == 0)：该用户之前未批准任何人。（否则 Z3 将生成一个反例，其中一些已获批准的用户窃取 WETH）

接下来，我们构建我们全新的状态，并通过与我们全新的存款人进行符号存款来更新它：

state = (eth_balances, balanceOf, allowance)
state = deposit(s, state, myUser, initialDeposit)

现在我们有了一个可以用来证明定理的起始状态。请注意，出于之前讨论的原因，我们不对我们的状态施加 任何其他假设 ——这意味着变量可以在任何 (合理) 的配置中。

执行符号交易

现在我们有了一个起始状态，我们在其上执行符号交易。这是相当简单的。以下是我们如何建模一个 任意 的符号 deposit 调用：

def symbolic_deposit(s, state, myUser):
    user = FreshConst(AddressSort, 'user')
    value = FreshConst(UintSort, 'value')

    s.add(user != WETH_Address)
    s.add(user != myUser)

    state = deposit(s, state, user, value)
    return state

我们用一个不受约束的 msg_sender 和 msg_value 调用我们的符号 deposit 实现。请注意，我们确实要求 msg_sender 不是 WETH 本身（因为 WETH 从未调用过其自己的任何函数），并且该用户不是我们的假设存款人。请注意，这里我们已隐含假设存款人不会在提取之前触碰他的资金。但是，如果没有此约束，求解器将生成无意义的反例，因为此约束是最终的 不 satisfiable 核心↗ 的一部分。

我们对所有外部函数采取类似的方式：deposit、withdraw、approve、transfer 和 transferFrom。

对于每个这些函数，我们首先执行符号交易。然后，我们在更新的状态中模拟从我们的假设存款人处进行符号提取。最后，我们要求求解器证明存款人的提取失败或存款人最终未能保留之前相同金额的资金的情况是 不满足 的。

请注意，在我们的 CHC 模型中，sat 结果是理想的，而在这个 BMC 模型中，unsat 结果是理想的。此外，在 CHC 中，我们从一个 具体的 初始状态开始，通过 递归 应用状态转移规则逐步扩展我们可达的状态集。而在这个 BMC 模型中，我们的起始状态是 符号的，但我们只执行一个 单一 的符号交易。这两个建模方法之间存在一些有趣的对偶关系。

结果

运行我们的 Z3Py 代码，我们证明了任何潜在的外部交易在有偿付能力状态下都会保持该状态的偿付能力。换句话说，偿付能力是不变的。我们还可以查询求解器以获取 不满足核心↗，这是所有实现不满足结果所需的最小化主张子集。

deposit
Unsat core:
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!9   line 190  symbolic_deposit  user != WETH_Address
* b!10  line 191  symbolic_deposit  user != myUser
* b!11  line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!14  line 267  proof_deposit     Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
withdraw
Unsat core:
* b!0   line 156  initial_state     ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!20  line 99   withdraw          UGE(eth_balances[WETH_Address], wad)
* b!18  line 202  symbolic_withdraw  user != myUser
* b!17  line 201  symbolic_withdraw  user != WETH_Address
* b!19  line 94   withdraw          UGE(balanceOf[msg_sender], wad)
* b!23  line 272  proof_withdraw    Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
approve
Unsat core:
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!31  line 277  proof_approve     Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
transfer
Unsat core:
* b!0   line 156  initial_state     ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!37  line 126  transferFrom      UGE(balanceOf[src], wad)
* b!36  line 224  symbolic_transfer  user != myUser
* b!41  line 282  proof_transfer    Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
transferFrom
Unsat core:
* b!0   line 156  initial_state     ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!3   line 162  initial_state     ForAll([a], allowance[myUser][a] == 0)
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!47  line 236  symbolic_transferFrom  user != myUser
* b!48  line 126  transferFrom      UGE(balanceOf[src], wad)
* b!49  line 130  transferFrom      Implies(p, UGE(allowance[src][msg_sender], wad))
* b!52  line 287  proof_transferFrom  Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok

不满足核心很有趣，因为它确切地告诉我们哪些主张对于智能合约的安全性是必须的，因此不能被删除！

未来工作

这项工作有几个局限性，这是未来研究的潜在方向。

首先，由于 WETH 合约非常简单，我们手动对各种功能进行了符号化。大量的手动建模和符号化可以通过正式验证框架自动化。这也将降低在构建模型时发生人为错误的可能性。

其次，我们在 BMC 模型中未考虑事件或返回值。这些对检查 WETH 是否符合 ERC-20 标准很重要。我们考虑将其排除在本工作的范围之外，因为我们这里只关心 WETH 的安全属性，而不是严格的 ERC-20 合规性。

第三，我们没有精确建模重入或程序间控制流。在 BMC 中，程序间控制流通常通过有界内联解决。然而，WETH 并未包含任何程序间调用，因此我们不必考虑这一点。此外，尽管由于使用原生 ether 存在重入的潜力，但 WETH 通过 .transfer 发送 ether，这施加了 2300 的Gas限制，这对于重入来说太低，不会构成真正的担忧。重入可以通过考虑重入带来的附加潜在转移和起始状态进行建模。

总结

WETH 是一个极其广泛、流行且关键的智能合约。我们证明了关于 WETH 的两个重要属性：（1）其 totalSupply 总是大于或等于存在的所有 WETH 代币的总和，以及（2）一个新的用户存入 eth 到 WETH 后，总是能够在稍后提取，无论在此期间发生了什么交易。我们还发现了 WETH 的 totalSupply 实现中的一个有趣但无害的特性，因为它不考虑 SELFDESTRUCT/coinbase eth 转移。

我们使用两种不同但互补的方法证明了这两个不变式。第一个是使用约束霍恩子句（CHC）。第二个则采用类似于有界模型检查（BMC）的方法。

通过 SMT 求解进行正式验证是一种广泛使用的方法。例如，它是 solc 内置 SMTchecker 的一部分，并且似乎在 Certora 等框架中被广泛使用。这种方法非常吸引人，因为定性上，SMT 求解器能够“神奇地”证明定理，所需时间与各种公式的位大小成多项式关系。 然而，在遵循此方法时，一个主要的挑战是证明时间不可接受地慢。即使约束系统是“正确的”，由于特定的 SMT 求解器（例如，Z3）没有“找到”证明，求解也可能非常缓慢。不过，在证明开发过程中我们可以使用一些启发式解决方案来改善这一点。

在开发证明时，将地址和 uint256 的位数（分别为 160 位和 256 位）大幅降低到，例如，4 位和 8 位通常是有用的。这有助于调试证明，因为即使 Z3 被困在“愚蠢”的暴力解法中，它仍然可能及时完成——而且 sat 模型或 unsat 证明将使解决方案的暴力性质变得明显（证明或模型将会非常庞大）。导致暴力证明的问题随后可以在这一缩小的模型中被迅速调试和解决。

在与求解器快速解析的“缩小”玩具模型工作后，然后可以逐渐“缩放回”原始大小，同时仔细测量证明运行时间如何随着模型大小的增大而变化。例如，你可能证明一个玩具模型，其中地址为 4 位，uint 为 8 位——然后可能为 16 和 16 位，再然后是 32 和 32 位，等等。如果你注意到证明时间在比特大小上保持线性（理想）或多项式（不太理想），这通常是有希望的。总体而言，这种方法可以帮助识别证明中瓶颈所在。然后，可以对这些瓶颈进行定向，通过手动向求解器添加“有用”的引理。

再次强调，现阶段全面自动化的解决方案似乎不存在。对于除最简单定理以外的所有定理，SMT 求解器通常没有足够的复杂性来证明所有期望的不变式，而无需人工干预或指导。例如，要证明第一个不变式，我们必须人为地向 Z3 提供有帮助的中间引理，以指导其向证明推进。在证明第二个不变式时，我们必须人为提供第一个不变式中证明的关键引理。没有 某种 程度的人为干预，似乎非常不可能有一个完全自动化的解决方案能够证明 WETH 的期望不变式。

WETH 是一个极其简单的合约。一个有趣的问题是，基于 SMT 的正式验证是否会扩展到更大的协议，尤其是涉及多个相互作用的智能合约的协议。正式验证更大协议是很理想的，因为除了 WETH，许多“关键”合约仍然存在。比如 Uniswap、Compound、Aave 和 Curve。在未来，我们希望能看到更多智能合约的正式验证得到采用。

关于我们

Zellic 专注于保障新兴技术的安全。我们的安全研究人员在最有价值的目标中发现了漏洞，范围涵盖从财富 500 强企业到 DeFi 巨头。

开发者、创始人和投资者信赖我们的安全评估，以便快速、自信地发布，并且没有关键漏洞。凭借我们在现实世界进攻性安全研究的背景，我们发现那些别人忽视的问题。

联系我们↗ 获得比其他审计更好的审核。真正的审核，而非走过场。

附注

1. 截至区块 15934960（2022 年 11 月 9 日），WETH 已进行 125,581,756 笔交易。此计数包括所有“顶层”交易，这些交易在任何时间点调用 WETH 合约，包括通过内部交易。交易不会被重复计算。 ↩

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