形式化验证 Solady WETH
- RareSkills
- 发布于 2026-02-14 11:17
- 阅读 15
本文详细介绍了如何使用 Certora Prover 对 Solady WETH 智能合约进行形式化验证。文章通过具体的 CVL 规则和不变式，深入分析了 WETH 的存取款功能及其核心不变性，包括处理以太坊余额、WETH 总供应量变化、事务回滚条件以及利用 ghost 变量和 hook 处理底层调用，最终展示了如何用 requireInvariant 优化验证。
形式化验证与Certora
形式化验证Solady WETH
最后更新于 2026年2月13日
导言
$ETH$ 在DeFi中广泛用于兑换、提供流动性、质押和抵押，它需要一个兼容ERC-20的版本，以便协议能够通过与其他代币相同的标准化接口与其交互。
这催生了Wrapped $ETH$（$WETH$），其原理很简单：存入原生 $ETH$ 会向用户的账户铸造等量的 $WETH$；而提取则会销毁相应的 $WETH$，并将原生 $ETH$ 返回给用户的账户。
在上一章中，我们形式化验证了一个典型ERC-20合约的基本属性。由于 $WETH$ 本身就是一个ERC-20，我们在这里不再重复这些规范，而是只关注 $WETH$ 特有的功能。我们将形式化验证 Solady WETH 的实现，该实现使用 inline assembly 进行 gas 优化。
需要形式化验证的 $WETH$ 属性
当用户存入 $ETH$ 时，他们必须收到等量的 $WETH$。当他们提款时，他们必须能够随时将该 $WETH$ 兑换成等量的 $ETH$。
这两个行为定义了 $WETH$ 合约除标准ERC-20功能之外的核心保证。为了维护这些保证，合约必须满足两个关键不变量：
- 合约持有的 $ETH$ 必须始终大于或等于 $WETH$ 总供应量。 这保证了所有 $WETH$ 持有者可以随时赎回其代币为 $ETH$，无论赎回顺序或时间。
- $WETH$ 总供应量必须始终大于或等于所有 $WETH$ 余额的总和。 这保证了合约不能分发超出其铸造数量的代币。
然而，我们不会形式化验证第二个不变量，因为Solady $WETH$ 合约继承的ERC-20实现不使用 mapping 来存储账户余额。相反，它使用计算出的槽位来对每个账户进行存储读写。
因此，验证这个不变量需要 $CVL$ “summarization”：我们需要 summarize 修改账户余额存储的函数，使用一个 ghost mapping 来镜像它们，并通过该 ghost state 来推理不变量。本章不讨论此主题。有关更多信息，请参阅Certora关于 summarization 的文档。
我们不验证这个不变量，而是形式化验证另一个：没有账户余额超过总供应量。这看似微不足道，但在 deposit 和 withdraw 规则依赖于与余额相关的前置条件时，它变得很有用。这个不变量允许我们使用 requireInvariant 替换这些假设，requireInvariant 提供了我们假设的那些前置条件确实有效的保证。
存入的 $ETH$ 等于收到的 $WETH$
当用户使用 deposit() 函数将 $ETH$ 存入合约时，他们的 $WETH$ 余额增加，他们的 $ETH$ 余额减少相同的数量。为了在 $CVL$ 中形式化验证此行为，我们按以下步骤进行：
- 设置前置条件：
- 发送者不得是合约本身（$e.msg.sender \neq currentContract$），因为自调用会破坏 $ETH$ 余额核算，并且没有执行路径允许此类调用。
- 发送者的 $WETH$ 余额加上存入的金额不得溢出（$balanceOf(e.msg.sender) + e.msg.value \le max_uint256$）。
- 在调用
deposit()之前记录用户的 $ETH$ 和 $WETH$ 余额。 - 以 $e.msg.value$ 中的 $ETH$ 金额调用
deposit()。 - 在调用
deposit()之后记录用户的 $ETH$ 和 $WETH$ 余额。 - 断言正确性条件：
- 最终的 $ETH$ 余额等于初始 $ETH$ 余额减去存入的金额。
- 最终的 $WETH$ 余额等于初始 $WETH$ 余额加上存入的金额。
这是 $CVL$ 规则实现：
Copyrule deposit_ethDepositedEqualsWethReceived(env e) {
require e.msg.sender != currentContract;
require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // will be replaced by an invariant
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}现在我们来详细解释一下。
前置条件
第一个前置条件指示 Prover 排除调用者 (msg.sender) 是合约本身的情况：
Copyrequire e.msg.sender != currentContract;如果没有这个前置条件，Prover 会假设调用者可以是 currentContract，这会导致规则失败。例如，如果合约向自己存入 $1$ $ETH$，其 $ETH$ 持有量不会发生净变化（因为它向自己发送和接收相同金额）。然而，合约仍然会铸造 $1$ $WETH$，导致断言 $ethBalanceAfter == ethBalanceBefore - e.msg.value$ 失败。
第二个前置条件，$require balanceOf(e.msg.sender) + e.msg.value \le max_uint256$，排除了在添加调用者的初始 $WETH$ 余额和 $ETH$ 存款时发生溢出的可能性。
由于 require 语句是 Prover 不验证的假设——它只是将其视为给定——我们需要在稍后的部分中将其作为不变量进行形式化证明。一旦证明，我们就可以使用 requireInvariant 将这个假定的前置条件替换为已验证的不变量。
在调用 deposit() 前后记录用户的 $ETH$ 和 $WETH$ 余额
设置所有前置条件后，我们必须在调用 deposit() 前后记录调用者的 $ETH$ 和 $WETH$ 余额。这些记录的值将用于断言中，以推理余额变化：
Copymathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);断言
第一个断言检查调用者的 $ETH$ 余额是否精确地减少了交易发送的 $ETH$ 金额。第二个断言检查调用者的 $WETH$ 余额是否精确地增加了存入的 $ETH$ 金额：
Copyassert ethBalanceAfter == ethBalanceBefore - e.msg.value; // ETH is deposited -- ETH balance decreases
assert wethBalanceAfter == wethBalanceBefore + e.msg.value; // WETH is received -- WETH balance increases这是 deposit_ethDepositedEqualsWethReceived 规则的已验证 Prover 运行 结果。
$ETH$ 存款增加 $WETH$ 总供应量
除了改变余额外，deposit() 调用的另一个预期效果是 $WETH$ totalSupply 的增加。以下 $CVL$ 规则捕获了此行为：
Copyrule deposit_ethDepositIncreasesWETHTotalSupply(env e) {
mathint totalSupplyBefore = totalSupply();
deposit(e);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
}变量 $totalSupplyBefore$ 和 $totalSupplyAfter$ 记录了在 deposit() 调用前后的总供应量值，以在断言中验证预期的变化。
由于 deposit() 函数内部调用 _mint()，因此 $WETH$ 的总供应量增加了存入的金额，如断言中所示：
Copyassert totalSupplyAfter == totalSupplyBefore + e.msg.value;请注意，这里没有前置条件 require msg.sender != currentContract，因为断言只涉及供应量的增加。无论发送者是谁，供应量都会增加存入的 $ETH$ 金额（$msg.value$）。
这是 deposit_ethDepositIncreasesWETHTotalSupply 规则的已验证 Prover 运行 结果。
验证 deposit() 中的revert原因
现在我们来验证 deposit() 函数的 revert 路径。我们希望检测它意外 revert 或未能 revert 的情况。
为了在 $CVL$ 中形式化验证此行为，我们按以下步骤进行：
- 设置前置条件：调用者的 $WETH$ 余额加上存入的金额不得溢出（$balanceOf(caller) + ethDeposit \le max_uint256$）。
- 在调用
deposit()之前记录 $WETH$totalSupply和调用者的 $ETH$ 余额。 - 使用
@withrevert标签调用deposit()，以允许规则观察revert。 - 使用
lastReverted，它返回一个布尔值，指示上次调用是否revert。 -
断言函数
revert当且仅当 ($\Leftrightarrow$) 以下任一条件为真：- 调用前调用者的 $ETH$ 余额小于存款金额（$e.msg.value$）。
- 调用前 $WETH$ 总供应量加上存款金额超过 $max_uint256$。
这是 $CVL$ 规则：
Copyrule deposit_revert(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}我们来进一步分解这条规则。
为了可读性，我们将 $e.msg.sender$ 和 $e.msg.value$ 分别赋值给 $caller$ 和 $ethDeposit$：
Copyaddress caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;下面的前置条件也出现在之前的 deposit_ethDepositedEqualsWethReceived() 规则中：
Copyrequire balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant它再次作为前置条件出现，而不是作为 revert 条件的一部分，进一步强调了对其进行形式化验证的必要性。
接下来，我们记录在调用 deposit() 函数之前 $totalSupplyBefore$（$WETH$ 总供应量）和调用者的 $nativeBalances$ 的值：
Copymathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];现在，我们使用 @withrevert 标签调用 deposit() 函数，并记录调用是否 revert：
Copydeposit@withrevert(e);
bool isLastReverted = lastReverted;最后，断言使用双条件运算符 ($\Leftrightarrow$)，并以析取式（使用 $OR$）列出所有 revert 情况：
- 当调用者的 $ETH$ 余额在调用前（$ethBalanceBefore$）小于存款金额（$e.msg.value$）时，函数会
revert。
这意味着调用者没有足够的 $ETH$ 进行存款。
- 当 $WETH$ 总供应量（$totalSupplyBefore$）加上 $ETH$ 存款会超过 $max_uint256$ 时，函数也会
revert。
由于每次存款都会铸造等量的 $WETH$，超过 uint256 限制将导致溢出。
Copyassert isLastReverted <=> (
ethBalanceBefore < ethDeposit || // the caller doesn't have enough eth to deposit
totalSupplyBefore + ethDeposit > max_uint256 // results in overflow
);前置条件 msg.sender != currentContract 是不必要的，因为 revert 条件涉及余额不足和溢出，这与调用者的身份无关。
这是 deposit_revert 规则的已验证 Prover 运行 结果。
提取的 $ETH$ 等于减少的 $WETH$
当用户从合约中提取 $ETH$ 时，他们的 $ETH$ 余额增加，他们的 $WETH$ 余额减少相同的数量。以下 $CVL$ 规则捕获了此行为：
Copyrule withdraw_ethWithdrawnEqualsWETHReduced(env e) {
uint256 amount;
require e.msg.sender != currentContract;
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw(e,amount);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;
}这遵循了 rule deposit_ethDepositedEqualsWethReceived() 的相同结构。到目前为止，模式应该很熟悉了：
- 设置前置条件
- 在调用
withdraw()之前记录调用者的 $ETH$ 和 $WETH$ 余额 - 调用
withdraw() - 之后记录调用者的 $ETH$ 和 $WETH$ 余额
Copyrequire e.msg.sender != currentContract;
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw(e,amount);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);现在，我们直接来看断言。
在下面的断言中，我们验证 $ETH$ 余额增加， $WETH$ 余额减少相同的提取 $amount$：
Copyassert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;前置条件 require msg.sender != currentContract 是必要的，因为自调用不会导致合约的 $ETH$ 余额发生变化（向自己存款不会产生净变化），这会导致断言 $ethBalanceAfter == ethBalanceBefore + amount$ 失败（一个误报）。
这是 withdraw_ethWithdrawnEqualsWETHReduced 规则的已验证 Prover 运行 结果。
提取的 $ETH$ 减少 $WETH$ 总供应量
当用户提取 $ETH$ 时，相应的 $WETH$ 金额会被销毁，从而减少总供应量。这是 withdraw() 函数的预期效果。以下 $CVL$ 规则捕获了此行为：
Copyrule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
uint256 amount;
require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}由于提取会使总供应量减少提取的金额（等于销毁的余额），因此以下前置条件通过要求没有单个余额超过总供应量来确保 totalSupply 减法不会下溢：
Copyrequire balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant与之前的规则一样，这个前置条件代表了一个必须在稍后形式化验证的假设。
接下来，我们遵循熟悉的模式，记录 withdraw 调用前后的 $WETH$ 总供应量：
Copymathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();然后我们断言 $WETH$ totalSupply 减少了预期的金额：
Copyassert totalSupplyAfter == totalSupplyBefore - amount;前置条件 require e.msg.sender != currentContract 在这里是不必要的，因为供应量减少（或供应量变化）与调用者是谁无关。
此规则确认在提款期间销毁 $WETH$ 会正确减少总供应量。这是已验证 Prover 运行 结果。
验证 withdraw() 中的revert原因
withdraw_revert 规则与 deposit_revert 规则遵循不同的模式。要理解原因，我们首先来看看 withdraw 函数：
Copy/// @dev Burns `amount` WETH of the caller and sends `amount` ETH to the caller.
function withdraw(uint256 amount) public virtual {
_burn(msg.sender, amount);
/// @solidity memory-safe-assembly
assembly {
// Transfer the ETH and check if it succeeded or not.
if iszero(call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)) {
mstore(0x00, 0xb12d13eb) // `ETHTransferFailed()`.
revert(0x1c, 0x04)
}
}
}除了实现其自身 revert 条件的 _burn() 函数外，withdraw() 函数还包含检查 $ETH$ 传输是否成功的 assembly 代码：
Copyassembly {
// Transfer the ETH and check whether it succeeded.
if iszero(call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)) {
mstore(0x00, 0xb12d13eb) // `ETHTransferFailed()`.
revert(0x1c, 0x04)
}
}iszero 表达式在 $ETH$ 传输失败时返回 true，这会触发 revert。否则，它返回 false，表示 $ETH$ 传输成功。为了验证这种 assembly 行为，我们使用 $CVL$ hook（CALL）来观察低级 $ETH$ 传输调用是否如预期 revert。
这是验证所有 withdraw() revert 条件（包括低级调用失败）的 $CVL$ 规则：
Copypersistent ghost bool g_lowLevelCallFail;
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
if (rc == 0) {
g_lowLevelCallFail = true;
} else {
g_lowLevelCallFail = false;
}
}
rule withdraw_revert(env e) {
uint256 amount; // the amount of eth to claim
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > wethBalanceBefore ||
e.msg.value != 0 ||
g_lowLevelCallFail
);
}让我们解释一下上面的规则。
下面这行是持久幽灵变量（persistent ghost variable）的声明：
Copypersistent ghost bool g_lowLevelCallFail;注意：有关常规幽灵变量（ghost）和持久幽灵变量（persistent ghost）之间区别的讨论，请参阅单独的章节“使用持久幽灵变量”。
幽灵变量由 CALL hook 更新。当调用 withdraw() 方法时，特别是由将 $ETH$ 传输给调用者的低级调用触发时，hook 会被触发。如果低级调用失败（$rc == 0$），幽灵变量 $g_lowLevelCallFail$ 被设置为 true；如果调用成功（$rc \neq 0$），则设置为 false，如下面的 CALL hook 所示：
Copyhook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
if (rc == 0) {
g_lowLevelCallFail = true;
} else {
g_lowLevelCallFail = false;
}
}这为 Prover 提供了一种跟踪 assembly 块内部 $ETH$ 传输成功/失败的方法。
现在我们来看规则。
像往常一样，我们在调用 withdraw() 函数之前记录余额：
Copymathint wethBalanceBefore = balanceOf(e.msg.sender);然后我们使用 @withrevert 标签调用 withdraw() 函数，并记录调用是否 revert：
Copywithdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;在下面的断言中，函数 revert 当且仅当 ($\Leftrightarrow$) 以下条件之一满足：
- 提取的 $amount$ 超过了调用者的 $WETH$ 余额（$wethBalanceBefore$）
这意味着调用者试图提取的 $ETH$ 超过了其 $WETH$ 余额所允许的范围。
- 随调用发送了 $ETH$
这是不允许的，因为 withdraw 不是一个 payable 函数。
- $ETH$ 传回给调用者失败
此条件通过使用 $g_lowLevelCallFail$ 幽灵变量的低级 CALL 结果进行跟踪。
Copyassert isLastReverted <=> (
amount > wethBalanceBefore || // insufficient balance: withdrawal amount exceeds weth balance
e.msg.value != 0 || // non-payable: ETH was sent to a non-payable function
g_lowLevelCallFail // transfer failure: low-level call ETH transfer failed
);这是 withdraw_revert 规则的已验证 Prover 运行 结果。
不变量：总 $ETH$ 存款大于或等于 $WETH$ 总供应量（偿付能力）
为了让用户能够使用其 $WETH$ 成功赎回 $ETH$，合约持有的 $ETH$ 必须始终大于或等于 $WETH$ 总供应量。以下是捕获此属性的 $CVL$ 不变量：
Copyinvariant ethDepositsAlwaysGTEWethTotalSupply()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}下面这行表达了不变量：
CopynativeBalances[currentContract] >= totalSupply()然而，这个不变量并非普遍成立。它仅在 preserved 块中定义的特定条件下成立。下面的 preserved 块要求调用者 ($e.msg.sender$) 不等于 currentContract。
Copypreserved with (env e) {
require e.msg.sender != currentContract;
}这并非巧合，这个 require 条件出现在以下规则中：
deposit_ethDepositedEqualsWethReceived()withdraw_ethWithdrawnEqualsWETHReduced()
很明显，这与 $ETH$ 存款和 $WETH$ 发行之间的核算有关。如果合约自调用并存入 $ETH$，则 $ETH$ 没有净收益，但 $WETH$ 仍可能被铸造，这会导致 totalSupply 超过实际的 $ETH$ 存款。
下一个 preserved 块要求 $msg.sender$ 的余额小于或等于 totalSupply()，这可以防止提款操作导致下溢：
Copypreserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}毫不奇怪，这个条件在相关规则中再次出现。虽然它在这里作为 withdraw() 的保留条件（preserved condition）出现，但之前它曾作为 withdraw_ethWithdrawDecreasesWETHSupply 规则中的前置条件出现。
在这两种情况下，目标都是防止与下溢相关的反例（counterexamples）。这是一个强有力的理由将其作为不变量进行证明，我们将在下一节中进行。
这是 ethDepositsAlwaysGTEWethTotalSupply 不变量的已验证 Prover 运行 结果。
不变量：没有账户余额超过 $WETH$ 总供应量
此不变量表示为 $balanceOf(address) \le totalSupply()$，保证了以下几点：
- 任何账户余额都不会超过总供应量。
- 因此，由于
totalSupply()本身不能超过max_uint256，单个账户余额也不会溢出。
在我们之前讨论的规则中，引入了以下前置条件以防止溢出：
Copyrule deposit_ethDepositedEqualsWethReceived(env e) {
...
require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // precondition
...
}Copyrule deposit_revert(env e) {
...
require balanceOf(caller) + ethDeposit <= max_uint256; // precondition
...
}在下面的 withdraw 规则中，添加了前置条件以防止下溢：
Copyrule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
...
require balanceOf(e.msg.sender) <= totalSupply(); // precondition
...
}在下面的 ethDepositsAlwaysGTEWethTotalSupply 不变量中，它也被用作防止下溢的保留条件：
Copyinvariant ethDepositsAlwaysGTEWethTotalSupply()
nativeBalances[currentContract] >= totalSupply()
{
...
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}下面的不变量通过形式化验证没有账户余额超过总供应量，直接解决了这些重复出现的前置条件：
Copyinvariant noAccountBalanceExceedsTotalSupply(env e1)
balanceOf(e1.msg.sender) <= totalSupply()
filtered {
f -> f.selector != sig:transfer(address,uint256).selector && // excludes standard ERC-20 transfer function from this invariant
f.selector != sig:transferFrom(address,address,uint256).selector // excludes standard ERC-20 transferFrom function from this invariant
}
{
preserved withdraw(uint256 amount) with (env e2) {
require e1.msg.sender == e2.msg.sender;
}
}我们来分解它。
下面这行是不变量：
CopybalanceOf(e1.msg.sender) <= totalSupply()我们使用 filtered 过滤掉了 transfer() 和 transferFrom()，因为这些函数计算并写入存储槽位，而不是使用 mapping 变量来存储账户余额。因此，跟踪账户余额需要使用 $CVL$ summaries 总结这些函数（这是一个超出本章范围的主题）。
Copyfiltered {
f -> f.selector != sig:transfer(address,uint256).selector &&
f.selector != sig:transferFrom(address,address,uint256).selector
}过滤掉 transfer() 和 transferFrom() 是合理的，因为只有 deposit() 和 withdraw()（它们分别调用 _mint() 和 _burn()）才能影响不变量。transfer() 和 transferFrom() 只是移动了总供应量中已经计入的代币。如果总供应量不正确，问题源于 deposit() 或 withdraw()，而不是传输。
如果Solady $WETH$ 使用了 mapping 变量（其设计有意避免），跟踪余额并定义此不变量将变得简单，并且这些过滤器将是不必要的。
话虽如此，与前置条件和保留块一样，应谨慎使用过滤器，因为它们可能会隐藏真实的错误。
最后，preserved 块要求 $e1.msg.sender$（我们在不变量中检查其余额的地址）等于 withdraw 函数执行期间的调用者：
Copy{
preserved withdraw(uint256 amount) with (env e2) {
require e1.msg.sender == e2.msg.sender;
}
}保留条件 $require e1.msg.sender == e2.msg.sender$ 阻止 Prover 在不调用 withdraw() 的账户上测试不变量。
withdraw() 函数触发销毁，这会减少总供应量，同时只减少调用者的余额。如果不变量检查一个余额没有变化的账户，Prover 可能会在销毁后观察到 $balanceOf(differentAccount) > totalSupply()$ 并报告一个虚假违规（false violation）。
通过要求不变量遵循执行 withdraw() 的相同地址，保留块强制检查适用于余额实际减少的账户。
这是已验证 Prover 运行 结果。
用 requireInvariant 替换前置条件
由于 noAccountBalanceExceedsTotalSupply() 现在已通过形式化验证，我们可以将前置条件和保留条件替换为以下规范中的这个不变量：
rule deposit_ethDepositedEqualsWethReceived()rule deposit_revert()rule withdraw_ethWithdrawDecreasesWETHSupply()invariant ethDepositsAlwaysGTEWethTotalSupply()
以下是使用 requireInvariant 重构的规则和不变量：
Copyrule deposit_ethDepositedEqualsWethReceived_withInvariant(env e) {
require e.msg.sender != currentContract;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
rule deposit_revert_withInvariant(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
rule withdraw_ethWithdrawDecreasesWETHSupply_withInvariant(env e) {
uint256 amount;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
invariant ethDepositsAlwaysGTEWethTotalSupply_withInvariant()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
requireInvariant noAccountBalanceExceedsTotalSupply(e);
}
}这是这些规则和不变量的已验证 Prover 运行 结果。
完整的 $CVL$ 规范和 Prover 运行
这是本章中编写的完整规范：
Copymethods {
function balanceOf(address) external returns (uint256) envfree;
function totalSupply() external returns (uint256) envfree;
}
persistent ghost bool g_lowLevelCallFail;
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
if (rc == 0) {
g_lowLevelCallFail = true;
} else {
g_lowLevelCallFail = false;
}
}
rule deposit_ethDepositedEqualsWethReceived(env e) {
require e.msg.sender != currentContract;
require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // will be replaced by an invariant
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
rule deposit_ethDepositedEqualsWethReceived_withInvariant(env e) {
require e.msg.sender != currentContract;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
rule deposit_ethDepositIncreasesWETHTotalSupply(env e) {
mathint totalSupplyBefore = totalSupply();
deposit(e);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
}
rule deposit_revert(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
rule deposit_revert_withInvariant(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
rule withdraw_ethWithdrawnEqualsWETHReduced(env e) {
uint256 amount;
require e.msg.sender != currentContract;
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw(e,amount);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;
}
rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
uint256 amount;
require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
rule withdraw_ethWithdrawDecreasesWETHSupply_withInvariant(env e) {
uint256 amount;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
rule withdraw_revert(env e) {
uint256 amount; // the amount of eth to claim
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > wethBalanceBefore ||
e.msg.value != 0 ||
g_lowLevelCallFail
);
}
invariant ethDepositsAlwaysGTEWethTotalSupply()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}
invariant ethDepositsAlwaysGTEWethTotalSupply_withInvariant()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
requireInvariant noAccountBalanceExceedsTotalSupply(e);
}
}
invariant noAccountBalanceExceedsTotalSupply(env e1)
balanceOf(e1.msg.sender) <= totalSupply()
filtered {
f -> f.selector != sig:transfer(address,uint256).selector &&
f.selector != sig:transferFrom(address,address,uint256).selector
}
{
preserved withdraw(uint256 amount) with (env e2) {
require e1.msg.sender == e2.msg.sender;
}
}这是本章讨论的 $WETH$ 规范的已验证 Prover 运行 结果。
本文是关于 使用Certora Prover进行形式化验证 系列文章的一部分。
- 原文链接： rareskills.io/post/certo...
- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
复制链接
Twitter分享
微信扫码分享
- RWA安全标准：ERC-3643 与 ERC-1400 比较 36 浏览
- 纵深防御智能合约工作流：超越静态检查表 68 浏览
- ERC-721 的部分参数化规则 0 浏览
- CVL 中的循环：路径爆炸与循环展开 0 浏览
- 参数化规则介绍 1 浏览
- 形式化验证介绍 2 浏览
- 约束规则中的幽灵变量 1 浏览
- 在CVL中测试msg.sender和msg.value 0 浏览
- Certora 中的不变量介绍 0 浏览
- 蕴涵运算符 1 浏览
- 方法属性介绍 1 浏览
- 持久化幽灵变量 0 浏览
