使用 Certora 形式化验证在外部审计师之前发现高危漏洞

Dacian 发布于 2024-11-30 阅读 1901

本文作者分享了使用 Certora Verification Language (CVL) 进行智能合约形式化验证的经验，通过将模糊测试中的不变量思想应用于 CVL，解决了之前在模糊测试中发现的真实漏洞的简化版本。文章详细对比了模糊测试与形式化验证的异同，并展示了使用 Certora 解决各种漏洞的实例，强调了 Certora 在漏洞检测方面的有效性和简洁性。

在 [DeFi Security Summit 2024](https://defisecuritysummit.org/conference-2024/) 上，我做了一个关于智能合约开发者如何在外部审计之前使用 [不变性模糊测试来发现高危漏洞](https://learnblockchain.cn/article/10147) 的研讨会，这是基于我在 Cyfrin 进行私有审计的真实经验。

由于模糊测试起初可能看起来令人望而却步，所以我提出了一个简单的学习方法，即 [“以不变性思考”](https://learnblockchain.cn/article/10147#heading-thinking-in-invariants)，任何开发者都可以学习并应用它来开始构建有效的不变性模糊测试套件。作为回应，许多研究人员和开发者联系我，询问是否可以使用形式化验证 (FV) 采用类似的方法，答案是响亮的“是”，但需要进行一些修改。

本文将展示如何使用 [Certora Verification Language](https://docs.certora.com/en/latest/docs/cvl/index.html) (CVL) 来解决我之前不变性模糊测试深入研究中简化的真实世界漏洞。Certora 非常慷慨地提供了一个免费套餐，任何人都可以注册，我不断地使用它来创建这些解决方案（包括 **许多** 失败的尝试），但仍然没有接近达到限制，所以 [今天就注册吧](https://www.certora.com/signup?plan=prover&utm=updraft)!

还要特别感谢：

- [Updraft Assembly & Formal Verification Course](https://updraft.cyfrin.io/courses/formal-verification)，它是免费的，非常适合学习 Certora！

- [alexzoid\_eth](https://x.com/alexzoid_eth)，他为改进一些解决方案提供了宝贵的帮助

- [kirsteinuri](https://x.com/kirsteinuri) 审阅了本文并提供了宝贵的更正

在我们开始研究 Certora 解决方案之前，让我们简要地研究一下使用不变性模糊器和 Certora 之间的一些重要区别。

## 不变性模糊测试 vs 形式化验证

关于“以不变性思考”的一切仍然适用，并从模糊测试延续到形式化验证中——我们需要指定 [有用的属性](https://github.com/Certora/Tutorials/blob/master/06.Lesson_ThinkingProperties/Categorizing_Properties.pdf) 才能有效地使用模糊测试和形式化验证。然而，一些值得注意的区别包括：

### Solidity vs Certora Verification Language (CVL)

我们的模糊器都是用 Solidity 编写的，但是当使用 Certora 时，我们使用 Certora 的特定领域语言 CVL 编写“规范”。这些规范用作 Certora “Prover” 的输入，它将规范中的规则与被验证的底层智能合约进行比较，以识别可能导致断言被违反的场景。用 CVL 编写规范需要一些时间来适应，但是非常强大，与笨重的模糊器相比，它允许创建优雅而简洁的解决方案，我们很快就会看到。

### 本地模糊测试 vs 云形式化验证

我们编写的模糊器都在本地运行，但是由于我们使用了 Chimera 框架，因此可以使用 [getrecon.xyz](https://getrecon.xyz/) 轻松地在云中运行它们。相反，Certora 的命令行工具将进行一些基本的错误检查和编译，然后将其发送到云进行执行；结果可能需要 30-60 秒才能在 Certora 的 Web 界面中可见。

### 模糊测试设置 vs 形式化验证关系

通常，对一个或多个智能合约的模糊测试将：

- 通过构造函数创建合约，将重要参数设置为特定值

- 调用任何初始化函数，设置角色并授予权限

- 使用 [“handler”](https://learnblockchain.cn/article/10147#heading-handlers-vs-no-handlers) 函数包装合约的底层函数，这些函数更新 ghost 变量并满足前提条件，从而减少浪费的模糊运行次数

在创建的环境中，模糊器会尝试许多随机的函数调用组合，试图打破定义的不变性。这种方法的一个重要结果是，`require` 语句中所有对参数值的限制都将被遵守，因此，如果模糊器打破了不变性，则很可能是一个有效的发现。

相反，当使用 Certora 时，没有“设置”函数，我们没有显式地创建合约，设置参数或编写任何 Solidity。相反，我们：

- 定义一个 `.conf` [configuration](https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html) 文件，其中包含一些基本信息 - 我们正在测试的合约和可选的 Certora 标志

- 编写一个 `.spec` [specification](https://docs.certora.com/en/latest/docs/cvl/overview.html) 文件，其中包含我们使用 CVL 的 Certora 规范，该规范使用 CVL `require` 语句定义不变性和对象之间的关系（例如存储位置或环境参数），以限制 Certora 通过达到无效状态来打破不变性

一个好处是，与笨重的模糊测试代码相比，Certora 规范可以非常简洁。但是，一个缺点是，底层合约中存在的一些限制可能需要在规范中使用 CVL `require` 语句复制，以防止 Certora 将存储槽设置为永远不可能的值，从而通过无效状态打破不变性。

### 模糊测试不变性 vs Certora `rule` 和 `invariant`

我们使用的所有 3 个模糊器通常具有相同类型的不变性；一个函数，要么返回一个布尔值 (Echidna/Medusa)，要么断言失败 (Foundry)。相反，Certora 有两种方法来实现“不变性”，即使用 `rule` 和 `invariant` 关键字。

- [`rule`](https://docs.certora.com/en/latest/docs/cvl/rules.html) 最好用于向 Certora 描述条件“场景”；这些条件使用一组 `require` 语句来表达，这些语句指定存储和/或环境之间的关系。这些条件之后是一个或多个 `assert` 或 [`satisfy`](https://docs.certora.com/en/latest/docs/cvl/statements.html#satisfy) 语句，这些语句是我们试图打破的实际属性

- [`invariant`](https://docs.certora.com/en/latest/docs/cvl/invariants.html) 不支持场景，最适合用于应该始终为真的简单布尔表达式

我个人认为 `rule` 是最强大的，所以我们的解决方案大多使用它。

### 模糊测试 Cheat Codes vs Certora `env`

在我们的模糊测试 handler 中，我们使用了许多 Cheat Codes，例如 `vm.prank` 来更改 `msg.sender` 或 `vm.warp` 来设置 `block.timestamp`。相反，Certora 有一个特殊的 [`env`](https://docs.certora.com/en/latest/docs/cvl/types.html#env) 类型，它是：

- 声明并作为第一个参数传递给底层函数调用

- 与 CVL `require` 语句一起使用，以约束环境属性，例如 `msg.sender` 或 `block.timestamp`

### 其他 Certora 功能

Certora 有许多非常强大的附加功能，包括 [参数化规则](https://docs.certora.com/en/latest/docs/user-guide/parametric.html) 和 [opcode hooks](https://docs.certora.com/en/latest/docs/user-guide/opcodes.html) - 将 [用户指南](https://docs.certora.com/en/latest/docs/user-guide/index.html) 打开作为方便的参考。还有许多重要的命令行参数，我们将其编码在 `.conf` 文件中，其中最重要的是 [`optimistic_loop`](https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-loop) 和 [`optimistic_fallback`](https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-fallback)。

现在我们已经了解了使用模糊测试和 Certora 之间的重要区别，让我们看看 Certora 规范对于我们在不变性模糊测试深入研究中解决的每个简化的真实世界漏洞是什么样的！

## 示例 1 - 闪电贷拒绝服务

规范：有 2 个合约 [`Receiver`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/02-unstoppable/ReceiverUnstoppable.sol) 和 [`Lender`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/02-unstoppable/UnstoppableLender.sol)。`Receiver` 有一个函数 `executeFlashLoan`，它调用 `Lender::flashLoan` 来进行闪电贷，重要的不变性是，如果 `Lender` 有足够的可用 token，`Receiver` 应该始终能够进行闪电贷。首先，我们创建配置文件 [`certora.conf`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/02-unstoppable/certora.conf)：

```json
{
  "files": [
    "src/02-unstoppable/ReceiverUnstoppable.sol",
    "src/02-unstoppable/UnstoppableLender.sol",
    "src/TestToken.sol"
  ],
  "verify": "ReceiverUnstoppable:test/02-unstoppable/certora.spec",
  "link": [
        "ReceiverUnstoppable:pool=UnstoppableLender",
        "UnstoppableLender:damnValuableToken=TestToken"
    ],
  "packages":[
        "@openzeppelin=lib/openzeppelin-contracts"
    ],
  "optimistic_loop": true
}
```

Certora 配置：

- 定义测试所需的 Solidity 源代码 `files`

- 标记要 `verify` 的合约和包含将发送到 Prover 的 Certora 规范的 `certora.spec` 文件

- 对于引用其他合约的合约，指示 Certora 将这些存储变量 `link` 到适当的合约类型

- 类似 Foundry 重映射的库路径所需的 `packages`

- 添加一个可选的命令行参数 `optimistic_loop`，以防止由于 Prover 的有界模型检查导致的不完整循环迭代产生不必要的反例

然后将我们的 Certora 规范放在 [`certora.spec`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/02-unstoppable/certora.spec) 中：

```solidity
using ReceiverUnstoppable as receiver;
using UnstoppableLender as lender;
using TestToken as token;

methods {
    // `dispatcher` 总结以防止 HAVOC
    function _.receiveTokens(address tokenAddress, uint256 amount) external => DISPATCHER(true);

// `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function token.balanceOf(address) external returns (uint256) envfree;
}

// executeFlashLoan() -> f() -> executeFlashLoan() 应该总是成功
rule executeFlashLoan_mustNotRevert(uint256 loanAmount) {
    // 强制执行有效的 msg.sender：
    // 1) 不是协议合约
    // 2) 等于 ReceiverUnstoppable::owner
    env e1;
    require e1.msg.sender != currentContract &&
            e1.msg.sender != lender &&
            e1.msg.sender != receiver &&
            e1.msg.sender != token &&
            e1.msg.sender == receiver.owner &&
            e1.msg.value  == 0; // 不可支付

// 强制执行存在足够的 token 以进行闪电贷
    require loanAmount > 0 && loanAmount <= token.balanceOf(lender);

// 第一次 executeFlashLoan() 成功
    executeFlashLoan(e1, loanAmount);

// 执行另一个任意成功的事务 f()
    env e2;
    require e2.msg.sender != currentContract &&
            e2.msg.sender != lender &&
            e2.msg.sender != receiver &&
            e2.msg.sender != token;
    method f;
    calldataarg args;
    f(e2, args);

// 第二次 executeFlashLoan() 应该总是成功；
    // 不应存在可能导致其失败的先前事务 f()
    executeFlashLoan@withrevert(e1, loanAmount);
    assert !lastReverted;
}
```

Certora 规范包含：

- 一个 `methods` 部分，为 Certora 提供有关底层合约中函数的其他信息，其中最常见的是将 `view` 函数标记为 `envfree`，因此在调用它们时不需要将 Certora 的特殊 `env` 类型作为输入参数传递

- 一个 `rule` 描述了我们希望测试的“场景”

- `require` 语句限制 `env` 环境，尤其是 `msg.sender`，并指示 Certora 满足前提条件，例如可用于闪电贷的足够 token

- 第一次 `executeFlashLoan` 调用始终成功

- 一个 [参数化](https://docs.certora.com/en/latest/docs/user-guide/parametric.html) 函数调用，指示 Certora 执行任何任意成功的函数调用 `f()`

- 第二次 `executeFlashLoan` 调用使用 `@withrevert` 来考虑此调用可能恢复的场景

- 如果之前的调用恢复，则断言失败，这意味着 Certora 打破了 `rule`，因此找到了有效的攻击路径

## 示例 2 - 奖励分配卡住

规范：一个 [`Proposal`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/03-proposal/Proposal.sol) 合约由 DAO 部署，其中包含一些 ETH，如果提案成功，则将其分配：

- `Proposal` 在投票结束或提案超时之前处于活动状态

- 在活动期间，符合条件的选民可以投票 `for` 或 `against`

- 如果达到法定人数，则应在 `for` 选民之间分配 ETH

- 否则，ETH 应退还给提案创建者

我们的 Certora 规范使用 `invariant` 构造，这与我们用于此挑战的 [模糊器不变性](https://learnblockchain.cn/article/10147#heading-example-2-reward-distribution-stuck) 非常相似，但请注意，完全没有任何设置、handler 或其他“基础设施”——一切都包含在 [`certora.spec`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/03-proposal/certora.spec) 文件中：

```solidity
methods {
    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function isActive() external returns (bool) envfree;
}

// 定义常量并在以后要求它们以防止 HAVOC 进入无效状态
definition MIN_FUNDING() returns uint256 = 1000000000000000000;
definition MIN_VOTERS()  returns uint256 = 3;
definition MAX_VOTERS()  returns uint256 = 9;

// 提案状态必须是：
// 1) 处于活动状态，余额 >= min_funding OR
// 2) 不处于活动状态，余额 == 0
invariant proposal_complete_all_rewards_distributed()
    (isActive()  && nativeBalances[currentContract] >= MIN_FUNDING()) ||
    (!isActive() && nativeBalances[currentContract] == 0)
{
    // 强制执行状态要求以防止 HAVOC 进入无效状态
    preserved {
        // 强制执行有效的允许总选民
        require(currentContract.s_totalAllowedVoters >= MIN_VOTERS() &&
                currentContract.s_totalAllowedVoters <= MAX_VOTERS() &&
                // 必须是奇数
                currentContract.s_totalAllowedVoters % 2 == 1);

// 强制执行有效赞成/反对票与当前总票数匹配
        require(currentContract.s_votersFor.length +
                currentContract.s_votersAgainst.length
                == currentContract.s_totalCurrentVotes);

// 强制执行当提案处于活动状态时，当前总票数必须最多为允许总选民的一半，
        // 因为一旦 >= 51% 的选票被投出，提案将自动完成
        require(!isActive() ||
                    (isActive() &&
                    currentContract.s_totalCurrentVotes <= currentContract.s_totalAllowedVoters/2)
                );
    }
}
```

由于没有设置，我们在 `invariant` 内的 `preserved` 块中使用 `require` 语句来强制执行关键合约参数的有效值。通常，智能合约的构造函数会强制执行这些限制，但 Certora 会在构造函数之后将存储槽设置为任意值。使用 `require` 语句，我们定义了限制可能值范围的关系，防止 Certora 由于无效状态而打破不变性。

同样值得注意的是 `currentContract` 的使用——一个特殊的关键字，允许直接访问正在验证的底层合约。

## 示例 3 - 投票权破坏

规范：一个 [`VotingNft`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/04-voting-nft/VotingNftForFuzz.sol) 合约：

- 允许用户将 ETH 作为抵押品存入他们的 NFT，以赋予 DAO 投票权

- NFT 可以由所有者创建，直到“权力计算开始时间”

- 一旦开始权力计算，所有 NFT 都会以最大投票权开始，对于未以存入 ETH 作为抵押品的 NFT，其投票权会随着时间而减少

- 已经减少的 NFT 投票权永远无法增加；存入所需的 ETH 抵押品只能防止任何未来的减少

使用 `rule` 构造，我们近似于我们 [Certora 规范](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/03-proposal/certora.spec) 中与 [模糊测试](https://learnblockchain.cn/article/10147#heading-example-3-voting-power-destruction) 相同的不变性：

```solidity
methods {
    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function getTotalPower()    external returns (uint256) envfree;
    function totalSupply()      external returns (uint256) envfree;
    function owner()            external returns (address) envfree;
    function ownerOf(uint256)   external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}

// 定义常量并在以后要求它们以防止 HAVOC 进入无效状态
definition PERCENTAGE_100() returns uint256 = 1000000000000000000000000000;

// 给定：safeMint() -> 权力计算开始时间 -> f()
// 不应存在 f()，当权力计算开始时，未经许可的攻击者可以将总权力设置为 0
rule total_power_gt_zero_power_calc_start(address to, uint256 tokenId) {
    // 强制执行在构造函数中设置的变量的基本健全性检查
    require currentContract.s_requiredCollateral > 0 &&
            currentContract.s_powerCalcTimestamp > 0 &&
            currentContract.s_maxNftPower > 0 &&
            currentContract.s_nftPowerReductionPercent > 0 &&
            currentContract.s_nftPowerReductionPercent < PERCENTAGE_100();

// 强制执行尚未创建任何 nft；实际上，由于 certora havoc，一些可能存在于存储中
    require totalSupply() == 0 && getTotalPower() == 0 && balanceOf(to) == 0;

// 强制执行 msg.sender 作为所有者，需要铸造 nft
    env e1;
    require e1.msg.sender == currentContract.owner();

// 强制执行 block.timestamp < 权力计算开始时间
    // 因此仍然可以铸造新的 nft
    require e1.block.timestamp < currentContract.s_powerCalcTimestamp;

// 第一次 safeMint() 成功
    safeMint(e1, to, tokenId);

// 健全性检查第一次铸造的结果
    assert totalSupply() == 1 && balanceOf(to) == 1 && ownerOf(tokenId) == to &&
           getTotalPower() == currentContract.s_maxNftPower;

// 在权力计算开始时间执行任何任意成功的事务，其中 msg.sender 不是 nft 所有者或管理员
    env e2;
    require e2.msg.sender != currentContract &&
            e2.msg.sender != to &&
            e2.msg.sender != currentContract.owner() &&
            balanceOf(e2.msg.sender) == 0 &&
            e2.block.timestamp == currentContract.s_powerCalcTimestamp;
    method f;
    calldataarg args;
    f(e2, args);

// 总权力不应等于 0
    assert getTotalPower() != 0;
}
```

再次注意 `require` 语句的使用，以防止初始存储状态被破坏，这会导致由于无效状态而违反不变性。

## 示例 4 - Token Sale Drain

规范：一个 [`TokenSale`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/05-token-sale/TokenSale.sol) 合约：

- 允许 DAO 出售其治理 `sellToken` 以换取另一个 `buyToken`

- Token Sale 仅适用于允许的用户，并且每个用户只能购买到每个用户的最大限制，以防止投票权集中

- 在我们的简化版本中，我们假设汇率为 1:1，并且 `sellToken` 的小数位数始终大于或等于 `buyToken`

这个底层合约使用两种 token；我们发现在配置中必须为每种 token 指定不同的合约，否则形式化验证将“通过”，但由于 [vacuity](https://docs.certora.com/projects/tutorials/en/latest/lesson2_started/vacuity.html) 实际上没有运行。[`certora.conf`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/05-token-sale/certora.conf) 看起来像这样：

```solidity
{
  "files": [
    "src/05-token-sale/TokenSale.sol",
    "src/TestToken.sol",
    "src/TestToken2.sol"
  ],
  "verify": "TokenSale:test/05-token-sale/certora.spec",
  "link": [
        "TokenSale:s_sellToken=TestToken",
        "TokenSale:s_buyToken=TestToken2"
  ],
  "packages":[
        "@openzeppelin=lib/openzeppelin-contracts"
  ],
  "optimistic_fallback": true,
  "optimistic_loop": true
}
```

对于 Certora [specification](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/05-token-sale/certora.spec)，我们使用每个不变性一个 `rule` 实现了两个 [fuzzer invariant](https://learnblockchain.cn/article/10147#heading-example-4-token-sale-drain)，效果很好：

```solidity
methods {
    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function getSellTokenSoldAmount() external returns (uint256) envfree;
}

// 定义常量并在以后要求它们以防止 HAVOC 进入无效状态
definition MIN_PRECISION_BUY() returns uint256 = 6;
definition PRECISION_SELL()    returns uint256 = 18;
definition FUNDING_MIN()       returns uint256 = 100;
definition BUYERS_MIN()        returns uint256 = 3;

// 由于 1:1 的交换率，购买的 token 数量应等于出售的 token 数量
rule tokens_bought_eq_tokens_sold(uint256 amountToBuy) {
    env e1;

uint8 sellTokenDecimals = currentContract.s_sellToken.decimals(e1);
    uint8 buyTokenDecimals  = currentContract.s_buyToken.decimals(e1);

// 强制执行在构造函数中设置的变量的基本健全性检查
    require currentContract.s_sellToken != currentContract.s_buyToken &&
            sellTokenDecimals == PRECISION_SELL()    &&
            buyTokenDecimals  >= MIN_PRECISION_BUY() &&
            buyTokenDecimals  <= PRECISION_SELL()    &&
            currentContract.s_sellTokenTotalAmount >= FUNDING_MIN() * 10 ^ sellTokenDecimals &&
            currentContract.s_maxTokensPerBuyer <= currentContract.s_sellTokenTotalAmount &&
            currentContract.s_totalBuyers >= BUYERS_MIN();

// 强制执行有效的 msg.sender
    require e1.msg.sender != currentContract.s_creator &&
            e1.msg.sender != currentContract.s_buyToken &&
            e1.msg.sender != currentContract.s_sellToken &&
            e1.msg.value == 0;

// 强制执行买方尚未购买任何正在出售的 token
    require currentContract.s_sellToken.balanceOf(e1, e1.msg.sender) == 0 &&
            getSellTokenSoldAmount() == 0;

// 强制执行买方拥有可用于购买正在出售的 token 的 token
    uint256 buyerBuyTokenBalPre = currentContract.s_buyToken.balanceOf(e1, e1.msg.sender);
    require buyerBuyTokenBalPre > 0 && amountToBuy > 0;

// 执行成功的 `buy` 事务
    buy(e1, amountToBuy);

// 买方必须收到一些来自 sale 的 token
    assert getSellTokenSoldAmount() > 0;
    uint256 buyerSellTokensBalPost = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);
    assert buyerSellTokensBalPost > 0;

uint256 buyerBuyTokenBalPost = currentContract.s_buyToken.balanceOf(e1, e1.msg.sender);

// 验证买方在考虑小数差异时，以 1:1 的比例支付了他们购买的 token
    assert getSellTokenSoldAmount() == (buyerBuyTokenBalPre - buyerBuyTokenBalPost)
                                       * 10 ^ (sellTokenDecimals - buyTokenDecimals);
}

// 此 규칙由 https://x.com/alexzoid_eth 提供
rule max_token_buy_per_user(env e1, env e2, uint256 amountToBuy1, uint256 amountToBuy2) {
    // 强制执行有效的初始状态
    require(currentContract.s_maxTokensPerBuyer <= currentContract.s_sellTokenTotalAmount);

// 强制执行在不同调用中的同一买方
    require e1.msg.sender == e2.msg.sender;
    require e1.msg.sender != currentContract && e1.msg.sender != currentContract.s_creator;

// 保存初始余额
    mathint balanceBefore = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);

// 阻止 ERC20 中的溢出（否则需要 totalSupply 和余额同步）
    require balanceBefore < max_uint128 && amountToBuy1 < max_uint128 && amountToBuy2 < max_uint128;

// 执行两个单独的 buy 事务
    buy(e1, amountToBuy1);
    buy(e2, amountToBuy2);

// 保存最终余额
    mathint balanceAfter = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);

// 验证同一用户购买的总数不得超过每个用户的最大限制
    mathint totalBuy = balanceAfter > balanceBefore ? balanceAfter - balanceBefore : 0;
    assert totalBuy <= currentContract.s_maxTokensPerBuyer;
}
```

## 示例 5 - 归属点增加

规范：[`Vesting`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/09-vesting/Vesting.sol) 合约将点分配给用户，这些点可用于在他们的归属期结束后兑换 token。合约在 `constructor` 中实现了一个 [初始不变性](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/09-vesting/Vesting.sol#L37)，确保所有点都被分配：

```solidity
require(totalPoints == TOTAL_POINTS, "Not enough points");
```

用户可以将他们的点转移到另一个地址，但除此之外，用户无法增加或减少他们分配的点，因此，个人用户点的总和应始终等于初始分配总数。

我没有重新实现与模糊器相同的不变性，而是使用了 Certora 的参数化规则来实现一个更简单的 [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/09-vesting/certora.spec#L4-L23)，实现了相同的结果：

```solidity
// 不应存在允许用户增加其分配点的函数 f()
rule user_cant_increase_points(address user) {
    require user != currentContract;

// 强制执行用户已分配一些点
    uint24 userPointsPre = currentContract.allocations[user].points;
    require userPointsPre > 0;

// 用户执行任何任意成功的事务 f()
    env e;
    require e.msg.sender == user;
    method f;
    calldataarg args;
    f(e, args);

// 验证不存在允许用户增加其分配点的事务
    assert userPointsPre >= currentContract.allocations[user].points;
}
```

这个优雅而简洁的解决方案精美地说明了 Certora 验证语言的强大特性，尤其是在使用参数化规则时。[alexzoid\_eth](https://x.com/alexzoid_eth) 还实现了另一个 [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/09-vesting/certora.spec#L26-L98)，它使用了与 [模糊器不变性](https://learnblockchain.cn/article/10147#heading-example-5-vesting-points-increase) 相同的想法：

```solidity
// 用户的个人点数总和应始终等于 TOTAL_POINTS
// 解决方案由 https://x.com/alexzoid_eth 提供
methods {
    function TOTAL_POINTS_PCT() external returns uint24 envfree => ALWAYS(100000);
}

// 跟踪点数已增加的用户的地址
ghost address targetUser;

// ghost 映射，用于跟踪每个用户地址的点数
ghost mapping (address => mathint) ghostPoints {
    axiom forall address user. ghostPoints[user] >= 0 && ghostPoints[user] <= max_uint24;
}

// hook 以验证存储读取是否与 ghost 状态匹配
hook Sload uint24 val allocations[KEY address user].points {
    require(require_uint24(ghostPoints[user]) == val);
}

// hook 以更新存储写入时的 ghost 状态
// 还跟踪第一个收到点数增加的用户
hook Sstore allocations[KEY address user].points uint24 val {
    // 仅当未设置且点数正在增加时才更新 targetUser
    targetUser = (targetUser == 0 && val > ghostPoints[user]) ? user : targetUser;
    ghostPoints[user] = val;
}

function initialize_constructor(address user1, address user2, address user3) {
    // 只有 user1、user2 和 user3 可以具有非零点数
    require(forall address user. user != user1 && user != user2 && user != user3 => ghostPoints[user] == 0);
    // 他们的点数总和必须等于总分配（100%）
    require(ghostPoints[user1] + ghostPoints[user2] + ghostPoints[user3] == TOTAL_POINTS_PCT());
}

function initialize_env(env e) {
    // 确保消息发送者是有效地址
    require(e.msg.sender != 0);
}

function initialize_users(address user1, address user2, address user3) {
    // 验证用户地址：
    // - 必须是非零地址
    require(user1 != 0 && user2 != 0 && user3 != 0);
    // - 必须是唯一地址
    require(user1 != user2 && user1 != user3 && user2 != user3);
    // 将 targetUser 初始化为零地址
    require(targetUser == 0);
}

// 验证总点数是否始终等于 TOTAL_POINTS_PCT (100%)
rule users_points_sum_eq_total_points(env e, address user1, address user2, address user3) {
    // 设置初始状态
    initialize_constructor(user1, user2, user3);
    initialize_env(e);
    initialize_users(user1, user2, user3);

// 使用任何参数执行任何方法
    method f;
    calldataarg args;
    f(e, args);

// 如果 targetUser 不是初始用户之一，则计算 targetUser 的点数
    mathint targetUserPoints = targetUser != user1 && targetUser != user2 && targetUser != user3 ? ghostPoints[targetUser] : 0;

// 断言总点数保持恒定为 100%
    assert(ghostPoints[user1] + ghostPoints[user2] + ghostPoints[user3] + targetUserPoints == TOTAL_POINTS_PCT());

// 所有其他地址必须具有零点数
    assert(forall address user. user != user1 && user != user2 && user != user3 && user != targetUser
        => ghostPoints[user] == 0
    );
}
```

## 示例 6 - 归属预先Claim Abuse

规范：[`VestingExt`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/10-vesting-ext/VestingExt.sol) 合约包含与以前的 `Vesting` 合约相同的功能，以及一个附加功能，允许用户 `preclaim` 其 token 分配的一部分，允许用户在其归属期到期之前获得有限数量的 token。

在实现 [fuzzer invariant](https://learnblockchain.cn/article/10147#heading-example-6-vesting-preclaim-abuse) 时，我验证了总 `preclaimed` 点数始终小于或等于最大可预先Claim的点数（这只是用户数量乘以每个用户的最大预先Claim点数）：

```solidity
function property_total_preclaimed_lt_eq_max_preclaimable() public view returns(bool result我实现了与 [fuzzer](https://learnblockchain.cn/article/10147#heading-example-7-operator-registry-corruption) 相同的**不变性**，但在 Certora 的 [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/11-op-reg/certora.spec) 中更加优雅和简洁，再次展示了 Certora 领域特定形式验证语言的强大功能，尤其是在使用参数化规则时：

```solidity
// 给定两个已注册的 operator，不应该存在任何 f() 会破坏
// operator_id : operator_address 之间唯一关系的情况
rule operator_addresses_have_unique_ids(address opAddr1, address opAddr2) {
    // 在 `operatorAddressToId` 映射中强制执行唯一的地址
    require opAddr1 != opAddr2;

uint128 op1AddrToId = currentContract.operatorAddressToId[opAddr1];
    uint128 op2AddrToId = currentContract.operatorAddressToId[opAddr2];

// 在 `operatorAddressToId` 映射中强制执行有效且唯一的 operator_ids
    require op1AddrToId != op2AddrToId && op1AddrToId > 0 && op2AddrToId > 0;

// 在 `operatorIdToAddress` 映射中强制执行匹配的地址
    require currentContract.operatorIdToAddress[op1AddrToId] == opAddr1 &&
            currentContract.operatorIdToAddress[op2AddrToId] == opAddr2;

// 执行任何任意成功的交易 f()
    env e;
    method f;
    calldataarg args;
    f(e, args);

// 验证是否没有交易会破坏
    // operator_id : operator_address 之间的唯一性属性
    assert currentContract.operatorIdToAddress[op1AddrToId] !=
           currentContract.operatorIdToAddress[op2AddrToId];
}

```

再次注意 `require` 语句的使用，指示 Certora 创建一个初始有效状态。

## 示例 8 - Liquidate Denial Of Service（清算拒绝服务）

规范：一个 [`LiquidateDos`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/12-liquidate-dos/LiquidateDos.sol) 合约允许交易者进入多个市场，并在每个市场中持有一个未平仓位。交易者也可以被清算：

- 在确定交易者是否可清算时，会考虑所有未平仓位

- 如果被清算，所有未平仓位都会为被清算的交易者平仓

- 清算不应因意外错误而失败

不幸的是，目前 Certora 不能用于意外的拒绝服务检查，因为 CVL 不返回 revert 的原因——它只提供 `lastReverted` 和 `lastHasThrown`，它们都是布尔值（如果使用 `revert` 操作码Hook，则提供 `size`）。Certora 在他们的 discord 中确认 _“我们有一个在 prover 中实现此功能的计划”_，因此一旦添加此功能，我们将进行更新。

## 示例 9 - Stability Pool Drain（稳定池耗尽）

规范：一个 [`StabilityPool`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/13-stability-pool/StabilityPool.sol) 合约，它：

- 允许用户存入 `debtToken`，该 `debtToken` 用于在清算期间偿还不良债务

- 作为交换，`debtToken` 存款人从清算期间查获的**抵押品代币**中获得一部分作为奖励

- 包含相当复杂的逻辑来计算 `debtToken` 存款人应获得的奖励份额

- 必须始终保持偿付能力；该池应始终有足够的**抵押品代币**来支付欠 `debtToken` 存款人的奖励

使用 `rule` 结构，我将 [fuzzer 中使用的**不变性**](https://learnblockchain.cn/article/10147#heading-example-9-stability-pool-drain) 转化为 Certora 能够 [求解](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/13-stability-pool/certora.spec) 的 “scenario”：

```solidity
methods {
    // `envfree` 定义，用于调用没有显式 `env` 的函数
    function getDepositorCollateralGain(address) external returns (uint256) envfree;
}

// 稳定池存款人不能耗尽稳定池；稳定池应始终持有足够的**抵押品代币**
// 来支付欠存款人的奖励
rule stability_pool_solvent(address spDep1, address spDep2) {
    // 强制执行地址合理性检查
    require spDep1 != spDep2 &&
            spDep1 != currentContract &&
            spDep1 != currentContract.debtToken &&
            spDep1 != currentContract.collateralToken &&
            spDep2 != currentContract &&
            spDep2 != currentContract.debtToken &&
            spDep2 != currentContract.collateralToken;

// 强制执行两个用户都没有 active deposits 或奖励
    require currentContract.accountDeposits[spDep1].amount     == 0 &&
            currentContract.accountDeposits[spDep1].timestamp  == 0 &&
            currentContract.depositSnapshots[spDep1].P         == 0 &&
            currentContract.depositSnapshots[spDep1].scale     == 0 &&
            currentContract.depositSnapshots[spDep1].epoch     == 0 &&
            currentContract.depositSums[spDep1]                == 0 &&
            currentContract.collateralGainsByDepositor[spDep1] == 0 &&
            currentContract.accountDeposits[spDep2].amount     == 0 &&
            currentContract.accountDeposits[spDep2].timestamp  == 0 &&
            currentContract.depositSnapshots[spDep2].P         == 0 &&
            currentContract.depositSnapshots[spDep2].scale     == 0 &&
            currentContract.depositSnapshots[spDep2].epoch     == 0 &&
            currentContract.depositSums[spDep2]                == 0 &&
            currentContract.collateralGainsByDepositor[spDep2] == 0;

// 强制执行两个用户都有代币可以存入稳定池
    env e;
    uint256 user1DebtTokens = currentContract.debtToken.balanceOf(e, spDep1);
    uint256 user2DebtTokens = currentContract.debtToken.balanceOf(e, spDep2);
    require user1DebtTokens >= 1000000000000000000 && user2DebtTokens >= 1000000000000000000 &&
            user1DebtTokens == user2DebtTokens;

// 两个用户将其 debt tokens 存入稳定池
    env e1;
    require e1.msg.sender == spDep1;
    provideToSP(e1, user1DebtTokens);
    env e2;
    require e2.msg.sender == spDep2;
    provideToSP(e2, user2DebtTokens);

// 稳定池用于抵消清算产生的债务
    uint256 debtTokensToOffset = require_uint256(user1DebtTokens + user2DebtTokens);
    uint256 seizedCollateral = debtTokensToOffset; // 1:1
    env e3;
    registerLiquidation(e3, debtTokensToOffset, seizedCollateral);

require(currentContract.collateralToken.balanceOf(e, currentContract) == seizedCollateral);

// 强制执行每个用户应获得相同的奖励，因为他们存入了相同的
    uint256 rewardPerUser = getDepositorCollateralGain(spDep1);
    require rewardPerUser > 0;
    require rewardPerUser == getDepositorCollateralGain(spDep2);

// 强制执行合约有足够的奖励代币来支付给两个用户
    require(currentContract.collateralToken.balanceOf(e, currentContract) >= require_uint256(rewardPerUser * 2));

// 第一个用户提取他们的奖励
    env e4;
    require e4.msg.sender == spDep1;
    claimCollateralGains(e4);

// 强制执行合约有足够的奖励代币来支付给第二个用户
    require(currentContract.collateralToken.balanceOf(e, currentContract) >= rewardPerUser);

// 第一个用户执行任何任意成功的交易 f()
    env e5;
    require e5.msg.sender == spDep1;
    method f;
    calldataarg args;
    f(e5, args);

// 第二个用户提取他们的奖励
    env e6;
    require e6.msg.sender == spDep2 &&
            e6.msg.value  == 0;
    claimCollateralGains@withrevert(e6);

// 验证第一个用户无法做任何会导致
    // 第二个用户的提款 revert 的事情
    assert !lastReverted;
}
```

再次注意大量使用 `require` 语句来防止 Certora 通过生成无效状态来破坏断言。

## 示例 10 - Collateral Priority Corruption（抵押品优先级损坏）

规范：一个 [`Priority`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/14-priority/Priority.sol) 合约，用于多抵押品借贷协议：

- 定义抵押品的清算优先级顺序

- 当发生清算时，风险最高的抵押品首先被清算，以便借款人剩余的抵押品篮子在清算后更加稳定

- 允许添加和删除抵押品；添加总是将新的抵押品放在优先级队列的末尾，而删除则保留现有的顺序，减去被删除的元素

在这里，我使用了与示例 #9 类似的方法，将 [fuzzer **不变性**](https://learnblockchain.cn/article/10147#heading-example-10-collateral-priority-corruption) 转换为一个`rule`，它描述了一个 [场景](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/14-priority/certora.spec) 然后验证 Certora 能够打破的断言：

```solidity
methods {
    // `envfree` 定义，用于调用没有显式 `env` 的函数
    function getCollateralAtPriority(uint8) external returns(uint8)   envfree;
    function containsCollateral(uint8)      external returns(bool)    envfree;
    function numCollateral()                external returns(uint256) envfree;
}

// 验证优先级队列顺序是否正确维护：
// - `addCollateral` 将新的 id 添加到队列的末尾
// - `removeCollateral` 保持现有顺序，减去被删除的 id
rule priority_order_correct() {
    // 需要没有初始抵押品以防止 HAVOC 破坏
    // EnumerableSet _positions -> _values 引用
    require numCollateral() == 0   && !containsCollateral(1) &&
            !containsCollateral(2) && !containsCollateral(3);

// 使用抵押品 id 顺序设置初始状态：1,2,3，这确保
    // EnumerableSet _positions -> _values 引用是正确的
    env e1;
    addCollateral(e1, 1);
    addCollateral(e1, 2);
    addCollateral(e1, 3);

// 健全性检查初始状态
    assert numCollateral() == 3  && containsCollateral(1) &&
           containsCollateral(2) && containsCollateral(3);

// 健全性检查初始顺序；这也验证了
    // `addCollateral` 是否按预期工作
    assert getCollateralAtPriority(0) == 1 &&
           getCollateralAtPriority(1) == 2 &&
           getCollateralAtPriority(2) == 3;

// 成功删除第一个 id 1
    removeCollateral(e1, 1);

// 验证它已被删除，并且其他 id 仍然存在
    assert numCollateral() == 2  && !containsCollateral(1) &&
           containsCollateral(2) && containsCollateral(3);

// 断言现有顺序 2,3 被保留，减去已删除的第一个 id 1
    assert getCollateralAtPriority(0) == 2 &&
           getCollateralAtPriority(1) == 3;
}
```

## 奖励 - Certora Foundry 插件

Certora 具有实验性的 Foundry 集成（[文档](https://docs.certora.com/en/latest/docs/cvl/foundry-integration.html)，[示例](https://github.com/Certora/Examples/tree/master/FoundryIntegration)），允许通过 Certora 的形式验证运行 Foundry 无状态模糊测试。考虑包含 Chimera 风格 `t()` 断言的函数 [`test_RarelyFalse`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/06-rarely-false/TargetFunctions.sol#L9-L25)，如果 `_rarelyFalse` 返回 `false`，则该断言会失败：

```solidity
uint256 constant private OFFSET = 1234;
uint256 constant private POW    = 80;
uint256 constant private LIMIT  = type(uint256).max - OFFSET;

// fuzzers 调用此函数
function test_RarelyFalse(uint256 n) external {
    // 输入前置条件
    n = between(n, 1, LIMIT);

// 要打破的断言
    t(_rarelyFalse(n + OFFSET, POW), "Should not be false");
}

// 要测试的实际实现
function _rarelyFalse(uint256 n, uint256 e) private pure returns(bool) {
    if(n % 2**e == 0) return false;
    return true;
}
```

在撰写本文时，所有的 Fuzzer (Foundry/Echidna/Medusa) 都无法找到 `_rarelyFalse` 返回 `false` 的情况，导致 `test_RarelyFalse` 中的断言失败——但 Certora 可以非常快速地找到它，而无需编写任何额外的代码！首先创建配置文件 [`certora.conf`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/06-rarely-false/certora.conf)，该文件除了通常的字段外，还有一个额外的可选 `foundry_tests_mode` 设置为 `true`：

```solidity
{
  "files": [\
    "test/06-rarely-false/RarelyFalseCryticToFoundry.sol"\
  ],
  "verify": "RarelyFalseCryticToFoundry:test/06-rarely-false/certora.spec",
  "packages":[\
        "@chimera=lib/chimera/src",\
        "forge-std=lib/forge-std/src"\
    ],
  "foundry_tests_mode": true
}
```

然后 [`certora.spec`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/06-rarely-false/certora.spec) 文件有这一行，它与测试完全无关：

```solidity
use builtin rule verifyFoundryFuzzTests;
```

这个简单的设置允许使用 Certora 对 Foundry 无状态模糊测试进行形式验证！

## 可能的改进

由于 Certora 已经创建了自己的领域特定语言，如果它包含一些 “syntactic sugar（语法糖）”，使常见模式更容易实现且不易出错，那就太好了。

一种常见的模式是使用 **ghost variable（幽灵变量）** 来跟踪映射中所有值的总和；这在示例 5 的第二个解决方案中使用。目前，这种模式实现起来相当繁琐且容易出错——如果提供一些语法糖，将其变成像这样的一行代码，那就更好了：

```solidity
// 对映射中的所有值求和
ghost mathint sumOfPoints = always_sum(currentContract.allocations.points);

// 对给定的一组键（这里是地址）的映射中的值求和
ghost mathint sumOfPoints = always_sum(currentContract.balances, users);
```

另一个潜在的改进是让 `certoraRun` 自动从 Hardhat/Foundry 配置文件中读取库路径，这样就不需要在 `.conf` 文件中复制这些路径。

“Syntactic sugar（语法糖）” 可以浓缩参数化函数调用，例如：

```solidity
// 调用任何东西
env e;
method f;
calldataarg args;
f(e, args);

// 调用任何东西语法糖
call_anything();

// 以 `user` 身份调用任何东西
env e5;
require e5.msg.sender == user;
method f;
calldataarg args;
f(e5, args);

// 以 `user` 身份调用任何东西语法糖
call_anything(msg.sender == user);
```

## 结论

从基于简化的真实世界漏洞的 10 个模糊测试挑战中，我们能够有效地编写 9 个 Certora 规范，这些规范正确地识别了相同的漏洞，仅因 CVL 缺乏对返回还原原因的支持而错过了挑战 8。在许多情况下，Certora 解决方案比相应的模糊器更优雅和简洁，因为：

- 无需编写设置或处理程序

- 由于 Certora 的强大功能，例如参数化规则

虽然学习 Certora 的领域特定语言可能听起来令人生畏，但使用 [Updraft 的免费课程](https://updraft.cyfrin.io/courses/formal-verification) 和官方 [用户指南](https://docs.certora.com/en/latest/docs/user-guide/index.html) 中的 Certora 课程，我能够在短短 7 天内学习到足够的 CVL 来编写这些解决方案并进行深入研究——如果我能做到，那么你也可以！

使用 Certora 进行形式验证是一种有效的工具，智能合约开发人员可以使用它在外部审计之前识别各种漏洞。Certora 慷慨的免费套餐允许开发人员和审计人员 [免费注册](https://www.certora.com/signup?plan=prover&utm=updraft) 并每月获得大量免费使用量，这对于大多数中小型协议来说已经足够了。

>- 原文链接： [dacian.me/find-highs-bef...](https://dacian.me/find-highs-before-external-auditors-using-certora-formal-verification)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

在 DeFi Security Summit 2024 上，我做了一个关于智能合约开发者如何在外部审计之前使用不变性模糊测试来发现高危漏洞的研讨会，这是基于我在 Cyfrin 进行私有审计的真实经验。

由于模糊测试起初可能看起来令人望而却步，所以我提出了一个简单的学习方法，即 “以不变性思考”，任何开发者都可以学习并应用它来开始构建有效的不变性模糊测试套件。作为回应，许多研究人员和开发者联系我，询问是否可以使用形式化验证 (FV) 采用类似的方法，答案是响亮的“是”，但需要进行一些修改。

本文将展示如何使用 Certora Verification Language (CVL) 来解决我之前不变性模糊测试深入研究中简化的真实世界漏洞。Certora 非常慷慨地提供了一个免费套餐，任何人都可以注册，我不断地使用它来创建这些解决方案（包括许多失败的尝试），但仍然没有接近达到限制，所以今天就注册吧!

还要特别感谢：

Updraft Assembly & Formal Verification Course，它是免费的，非常适合学习 Certora！
alexzoid_eth，他为改进一些解决方案提供了宝贵的帮助
kirsteinuri 审阅了本文并提供了宝贵的更正

在我们开始研究 Certora 解决方案之前，让我们简要地研究一下使用不变性模糊器和 Certora 之间的一些重要区别。

不变性模糊测试 vs 形式化验证

关于“以不变性思考”的一切仍然适用，并从模糊测试延续到形式化验证中——我们需要指定有用的属性才能有效地使用模糊测试和形式化验证。然而，一些值得注意的区别包括：

Solidity vs Certora Verification Language (CVL)

本地模糊测试 vs 云形式化验证

我们编写的模糊器都在本地运行，但是由于我们使用了 Chimera 框架，因此可以使用 getrecon.xyz 轻松地在云中运行它们。相反，Certora 的命令行工具将进行一些基本的错误检查和编译，然后将其发送到云进行执行；结果可能需要 30-60 秒才能在 Certora 的 Web 界面中可见。

模糊测试设置 vs 形式化验证关系

通常，对一个或多个智能合约的模糊测试将：

通过构造函数创建合约，将重要参数设置为特定值
调用任何初始化函数，设置角色并授予权限
使用 “handler” 函数包装合约的底层函数，这些函数更新 ghost 变量并满足前提条件，从而减少浪费的模糊运行次数

在创建的环境中，模糊器会尝试许多随机的函数调用组合，试图打破定义的不变性。这种方法的一个重要结果是，require 语句中所有对参数值的限制都将被遵守，因此，如果模糊器打破了不变性，则很可能是一个有效的发现。

相反，当使用 Certora 时，没有“设置”函数，我们没有显式地创建合约，设置参数或编写任何 Solidity。相反，我们：

定义一个 .conf configuration 文件，其中包含一些基本信息 - 我们正在测试的合约和可选的 Certora 标志
编写一个 .spec specification 文件，其中包含我们使用 CVL 的 Certora 规范，该规范使用 CVL require 语句定义不变性和对象之间的关系（例如存储位置或环境参数），以限制 Certora 通过达到无效状态来打破不变性

一个好处是，与笨重的模糊测试代码相比，Certora 规范可以非常简洁。但是，一个缺点是，底层合约中存在的一些限制可能需要在规范中使用 CVL require 语句复制，以防止 Certora 将存储槽设置为永远不可能的值，从而通过无效状态打破不变性。

模糊测试不变性 vs Certora `rule` 和 `invariant`

我们使用的所有 3 个模糊器通常具有相同类型的不变性；一个函数，要么返回一个布尔值 (Echidna/Medusa)，要么断言失败 (Foundry)。相反，Certora 有两种方法来实现“不变性”，即使用 rule 和 invariant 关键字。

rule 最好用于向 Certora 描述条件“场景”；这些条件使用一组 require 语句来表达，这些语句指定存储和/或环境之间的关系。这些条件之后是一个或多个 assert 或 satisfy 语句，这些语句是我们试图打破的实际属性
invariant 不支持场景，最适合用于应该始终为真的简单布尔表达式

我个人认为 rule 是最强大的，所以我们的解决方案大多使用它。

模糊测试 Cheat Codes vs Certora `env`

在我们的模糊测试 handler 中，我们使用了许多 Cheat Codes，例如 vm.prank 来更改 msg.sender 或 vm.warp 来设置 block.timestamp。相反，Certora 有一个特殊的 env 类型，它是：

声明并作为第一个参数传递给底层函数调用
与 CVL require 语句一起使用，以约束环境属性，例如 msg.sender 或 block.timestamp

其他 Certora 功能

Certora 有许多非常强大的附加功能，包括参数化规则和 opcode hooks - 将用户指南打开作为方便的参考。还有许多重要的命令行参数，我们将其编码在 .conf 文件中，其中最重要的是 optimistic_loop 和 optimistic_fallback。

示例 1 - 闪电贷拒绝服务

规范：有 2 个合约 Receiver 和 Lender。Receiver 有一个函数 executeFlashLoan，它调用 Lender::flashLoan 来进行闪电贷，重要的不变性是，如果 Lender 有足够的可用 token，Receiver 应该始终能够进行闪电贷。首先，我们创建配置文件 certora.conf：

{
  "files": [
    "src/02-unstoppable/ReceiverUnstoppable.sol",
    "src/02-unstoppable/UnstoppableLender.sol",
    "src/TestToken.sol"
  ],
  "verify": "ReceiverUnstoppable:test/02-unstoppable/certora.spec",
  "link": [
        "ReceiverUnstoppable:pool=UnstoppableLender",
        "UnstoppableLender:damnValuableToken=TestToken"
    ],
  "packages":[
        "@openzeppelin=lib/openzeppelin-contracts"
    ],
  "optimistic_loop": true
}

Certora 配置：

定义测试所需的 Solidity 源代码 files
标记要 verify 的合约和包含将发送到 Prover 的 Certora 规范的 certora.spec 文件
对于引用其他合约的合约，指示 Certora 将这些存储变量 link 到适当的合约类型
类似 Foundry 重映射的库路径所需的 packages
添加一个可选的命令行参数 optimistic_loop，以防止由于 Prover 的有界模型检查导致的不完整循环迭代产生不必要的反例

然后将我们的 Certora 规范放在 certora.spec 中：

using ReceiverUnstoppable as receiver;
using UnstoppableLender as lender;
using TestToken as token;

methods {
    // `dispatcher` 总结以防止 HAVOC
    function _.receiveTokens(address tokenAddress, uint256 amount) external => DISPATCHER(true);

    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function token.balanceOf(address) external returns (uint256) envfree;
}

// executeFlashLoan() -> f() -> executeFlashLoan() 应该总是成功
rule executeFlashLoan_mustNotRevert(uint256 loanAmount) {
    // 强制执行有效的 msg.sender：
    // 1) 不是协议合约
    // 2) 等于 ReceiverUnstoppable::owner
    env e1;
    require e1.msg.sender != currentContract &&
            e1.msg.sender != lender &&
            e1.msg.sender != receiver &&
            e1.msg.sender != token &&
            e1.msg.sender == receiver.owner &&
            e1.msg.value  == 0; // 不可支付

    // 强制执行存在足够的 token 以进行闪电贷
    require loanAmount > 0 && loanAmount &lt;= token.balanceOf(lender);

    // 第一次 executeFlashLoan() 成功
    executeFlashLoan(e1, loanAmount);

    // 执行另一个任意成功的事务 f()
    env e2;
    require e2.msg.sender != currentContract &&
            e2.msg.sender != lender &&
            e2.msg.sender != receiver &&
            e2.msg.sender != token;
    method f;
    calldataarg args;
    f(e2, args);

    // 第二次 executeFlashLoan() 应该总是成功；
    // 不应存在可能导致其失败的先前事务 f()
    executeFlashLoan@withrevert(e1, loanAmount);
    assert !lastReverted;
}

Certora 规范包含：

一个 methods 部分，为 Certora 提供有关底层合约中函数的其他信息，其中最常见的是将 view 函数标记为 envfree，因此在调用它们时不需要将 Certora 的特殊 env 类型作为输入参数传递
一个 rule 描述了我们希望测试的“场景”
require 语句限制 env 环境，尤其是 msg.sender，并指示 Certora 满足前提条件，例如可用于闪电贷的足够 token
第一次 executeFlashLoan 调用始终成功
一个参数化函数调用，指示 Certora 执行任何任意成功的函数调用 f()
第二次 executeFlashLoan 调用使用 @withrevert 来考虑此调用可能恢复的场景
如果之前的调用恢复，则断言失败，这意味着 Certora 打破了 rule，因此找到了有效的攻击路径

示例 2 - 奖励分配卡住

规范：一个 Proposal 合约由 DAO 部署，其中包含一些 ETH，如果提案成功，则将其分配：

Proposal 在投票结束或提案超时之前处于活动状态
在活动期间，符合条件的选民可以投票 for 或 against
如果达到法定人数，则应在 for 选民之间分配 ETH
否则，ETH 应退还给提案创建者

我们的 Certora 规范使用 invariant 构造，这与我们用于此挑战的模糊器不变性非常相似，但请注意，完全没有任何设置、handler 或其他“基础设施”——一切都包含在 certora.spec 文件中：

methods {
    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function isActive() external returns (bool) envfree;
}

// 定义常量并在以后要求它们以防止 HAVOC 进入无效状态
definition MIN_FUNDING() returns uint256 = 1000000000000000000;
definition MIN_VOTERS()  returns uint256 = 3;
definition MAX_VOTERS()  returns uint256 = 9;

// 提案状态必须是：
// 1) 处于活动状态，余额 >= min_funding OR
// 2) 不处于活动状态，余额 == 0
invariant proposal_complete_all_rewards_distributed()
    (isActive()  && nativeBalances[currentContract] >= MIN_FUNDING()) ||
    (!isActive() && nativeBalances[currentContract] == 0)
{
    // 强制执行状态要求以防止 HAVOC 进入无效状态
    preserved {
        // 强制执行有效的允许总选民
        require(currentContract.s_totalAllowedVoters >= MIN_VOTERS() &&
                currentContract.s_totalAllowedVoters &lt;= MAX_VOTERS() &&
                // 必须是奇数
                currentContract.s_totalAllowedVoters % 2 == 1);

        // 强制执行有效赞成/反对票与当前总票数匹配
        require(currentContract.s_votersFor.length +
                currentContract.s_votersAgainst.length
                == currentContract.s_totalCurrentVotes);

        // 强制执行当提案处于活动状态时，当前总票数必须最多为允许总选民的一半，
        // 因为一旦 >= 51% 的选票被投出，提案将自动完成
        require(!isActive() ||
                    (isActive() &&
                    currentContract.s_totalCurrentVotes &lt;= currentContract.s_totalAllowedVoters/2)
                );
    }
}

由于没有设置，我们在 invariant 内的 preserved 块中使用 require 语句来强制执行关键合约参数的有效值。通常，智能合约的构造函数会强制执行这些限制，但 Certora 会在构造函数之后将存储槽设置为任意值。使用 require 语句，我们定义了限制可能值范围的关系，防止 Certora 由于无效状态而打破不变性。

同样值得注意的是 currentContract 的使用——一个特殊的关键字，允许直接访问正在验证的底层合约。

示例 3 - 投票权破坏

规范：一个 VotingNft 合约：

允许用户将 ETH 作为抵押品存入他们的 NFT，以赋予 DAO 投票权
NFT 可以由所有者创建，直到“权力计算开始时间”
一旦开始权力计算，所有 NFT 都会以最大投票权开始，对于未以存入 ETH 作为抵押品的 NFT，其投票权会随着时间而减少
已经减少的 NFT 投票权永远无法增加；存入所需的 ETH 抵押品只能防止任何未来的减少

使用 rule 构造，我们近似于我们 Certora 规范中与模糊测试相同的不变性：

methods {
    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function getTotalPower()    external returns (uint256) envfree;
    function totalSupply()      external returns (uint256) envfree;
    function owner()            external returns (address) envfree;
    function ownerOf(uint256)   external returns (address) envfree;
    function balanceOf(address) external returns (uint256) envfree;
}

// 定义常量并在以后要求它们以防止 HAVOC 进入无效状态
definition PERCENTAGE_100() returns uint256 = 1000000000000000000000000000;

// 给定：safeMint() -> 权力计算开始时间 -> f()
// 不应存在 f()，当权力计算开始时，未经许可的攻击者可以将总权力设置为 0
rule total_power_gt_zero_power_calc_start(address to, uint256 tokenId) {
    // 强制执行在构造函数中设置的变量的基本健全性检查
    require currentContract.s_requiredCollateral > 0 &&
            currentContract.s_powerCalcTimestamp > 0 &&
            currentContract.s_maxNftPower > 0 &&
            currentContract.s_nftPowerReductionPercent > 0 &&
            currentContract.s_nftPowerReductionPercent &lt; PERCENTAGE_100();

    // 强制执行尚未创建任何 nft；实际上，由于 certora havoc，一些可能存在于存储中
    require totalSupply() == 0 && getTotalPower() == 0 && balanceOf(to) == 0;

    // 强制执行 msg.sender 作为所有者，需要铸造 nft
    env e1;
    require e1.msg.sender == currentContract.owner();

    // 强制执行 block.timestamp &lt; 权力计算开始时间
    // 因此仍然可以铸造新的 nft
    require e1.block.timestamp &lt; currentContract.s_powerCalcTimestamp;

    // 第一次 safeMint() 成功
    safeMint(e1, to, tokenId);

    // 健全性检查第一次铸造的结果
    assert totalSupply() == 1 && balanceOf(to) == 1 && ownerOf(tokenId) == to &&
           getTotalPower() == currentContract.s_maxNftPower;

    // 在权力计算开始时间执行任何任意成功的事务，其中 msg.sender 不是 nft 所有者或管理员
    env e2;
    require e2.msg.sender != currentContract &&
            e2.msg.sender != to &&
            e2.msg.sender != currentContract.owner() &&
            balanceOf(e2.msg.sender) == 0 &&
            e2.block.timestamp == currentContract.s_powerCalcTimestamp;
    method f;
    calldataarg args;
    f(e2, args);

    // 总权力不应等于 0
    assert getTotalPower() != 0;
}

再次注意 require 语句的使用，以防止初始存储状态被破坏，这会导致由于无效状态而违反不变性。

示例 4 - Token Sale Drain

规范：一个 TokenSale 合约：

允许 DAO 出售其治理 sellToken 以换取另一个 buyToken
Token Sale 仅适用于允许的用户，并且每个用户只能购买到每个用户的最大限制，以防止投票权集中
在我们的简化版本中，我们假设汇率为 1:1，并且 sellToken 的小数位数始终大于或等于 buyToken

这个底层合约使用两种 token；我们发现在配置中必须为每种 token 指定不同的合约，否则形式化验证将“通过”，但由于 vacuity 实际上没有运行。certora.conf 看起来像这样：

{
  "files": [
    "src/05-token-sale/TokenSale.sol",
    "src/TestToken.sol",
    "src/TestToken2.sol"
  ],
  "verify": "TokenSale:test/05-token-sale/certora.spec",
  "link": [
        "TokenSale:s_sellToken=TestToken",
        "TokenSale:s_buyToken=TestToken2"
  ],
  "packages":[
        "@openzeppelin=lib/openzeppelin-contracts"
  ],
  "optimistic_fallback": true,
  "optimistic_loop": true
}

对于 Certora specification，我们使用每个不变性一个 rule 实现了两个 fuzzer invariant，效果很好：

methods {
    // `envfree` 定义，用于在没有显式 `env` 的情况下调用函数
    function getSellTokenSoldAmount() external returns (uint256) envfree;
}

// 定义常量并在以后要求它们以防止 HAVOC 进入无效状态
definition MIN_PRECISION_BUY() returns uint256 = 6;
definition PRECISION_SELL()    returns uint256 = 18;
definition FUNDING_MIN()       returns uint256 = 100;
definition BUYERS_MIN()        returns uint256 = 3;

// 由于 1:1 的交换率，购买的 token 数量应等于出售的 token 数量
rule tokens_bought_eq_tokens_sold(uint256 amountToBuy) {
    env e1;

    uint8 sellTokenDecimals = currentContract.s_sellToken.decimals(e1);
    uint8 buyTokenDecimals  = currentContract.s_buyToken.decimals(e1);

    // 强制执行在构造函数中设置的变量的基本健全性检查
    require currentContract.s_sellToken != currentContract.s_buyToken &&
            sellTokenDecimals == PRECISION_SELL()    &&
            buyTokenDecimals  >= MIN_PRECISION_BUY() &&
            buyTokenDecimals  &lt;= PRECISION_SELL()    &&
            currentContract.s_sellTokenTotalAmount >= FUNDING_MIN() * 10 ^ sellTokenDecimals &&
            currentContract.s_maxTokensPerBuyer &lt;= currentContract.s_sellTokenTotalAmount &&
            currentContract.s_totalBuyers >= BUYERS_MIN();

    // 强制执行有效的 msg.sender
    require e1.msg.sender != currentContract.s_creator &&
            e1.msg.sender != currentContract.s_buyToken &&
            e1.msg.sender != currentContract.s_sellToken &&
            e1.msg.value == 0;

    // 强制执行买方尚未购买任何正在出售的 token
    require currentContract.s_sellToken.balanceOf(e1, e1.msg.sender) == 0 &&
            getSellTokenSoldAmount() == 0;

    // 强制执行买方拥有可用于购买正在出售的 token 的 token
    uint256 buyerBuyTokenBalPre = currentContract.s_buyToken.balanceOf(e1, e1.msg.sender);
    require buyerBuyTokenBalPre > 0 && amountToBuy > 0;

    // 执行成功的 `buy` 事务
    buy(e1, amountToBuy);

    // 买方必须收到一些来自 sale 的 token
    assert getSellTokenSoldAmount() > 0;
    uint256 buyerSellTokensBalPost = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);
    assert buyerSellTokensBalPost > 0;

    uint256 buyerBuyTokenBalPost = currentContract.s_buyToken.balanceOf(e1, e1.msg.sender);

    // 验证买方在考虑小数差异时，以 1:1 的比例支付了他们购买的 token
    assert getSellTokenSoldAmount() == (buyerBuyTokenBalPre - buyerBuyTokenBalPost)
                                       * 10 ^ (sellTokenDecimals - buyTokenDecimals);
}

// 此 규칙由 https://x.com/alexzoid_eth 提供
rule max_token_buy_per_user(env e1, env e2, uint256 amountToBuy1, uint256 amountToBuy2) {
    // 强制执行有效的初始状态
    require(currentContract.s_maxTokensPerBuyer &lt;= currentContract.s_sellTokenTotalAmount);

    // 强制执行在不同调用中的同一买方
    require e1.msg.sender == e2.msg.sender;
    require e1.msg.sender != currentContract && e1.msg.sender != currentContract.s_creator;

    // 保存初始余额
    mathint balanceBefore = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);

    // 阻止 ERC20 中的溢出（否则需要 totalSupply 和余额同步）
    require balanceBefore &lt; max_uint128 && amountToBuy1 &lt; max_uint128 && amountToBuy2 &lt; max_uint128;

    // 执行两个单独的 buy 事务
    buy(e1, amountToBuy1);
    buy(e2, amountToBuy2);

    // 保存最终余额
    mathint balanceAfter = currentContract.s_sellToken.balanceOf(e1, e1.msg.sender);

    // 验证同一用户购买的总数不得超过每个用户的最大限制
    mathint totalBuy = balanceAfter > balanceBefore ? balanceAfter - balanceBefore : 0;
    assert totalBuy &lt;= currentContract.s_maxTokensPerBuyer;
}

示例 5 - 归属点增加

规范：Vesting 合约将点分配给用户，这些点可用于在他们的归属期结束后兑换 token。合约在 constructor 中实现了一个初始不变性，确保所有点都被分配：

require(totalPoints == TOTAL_POINTS, "Not enough points");

用户可以将他们的点转移到另一个地址，但除此之外，用户无法增加或减少他们分配的点，因此，个人用户点的总和应始终等于初始分配总数。

我没有重新实现与模糊器相同的不变性，而是使用了 Certora 的参数化规则来实现一个更简单的 rule，实现了相同的结果：

// 不应存在允许用户增加其分配点的函数 f()
rule user_cant_increase_points(address user) {
    require user != currentContract;

    // 强制执行用户已分配一些点
    uint24 userPointsPre = currentContract.allocations[user].points;
    require userPointsPre > 0;

    // 用户执行任何任意成功的事务 f()
    env e;
    require e.msg.sender == user;
    method f;
    calldataarg args;
    f(e, args);

    // 验证不存在允许用户增加其分配点的事务
    assert userPointsPre >= currentContract.allocations[user].points;
}

这个优雅而简洁的解决方案精美地说明了 Certora 验证语言的强大特性，尤其是在使用参数化规则时。alexzoid_eth 还实现了另一个 rule，它使用了与模糊器不变性相同的想法：

// 用户的个人点数总和应始终等于 TOTAL_POINTS
// 解决方案由 https://x.com/alexzoid_eth 提供
methods {
    function TOTAL_POINTS_PCT() external returns uint24 envfree => ALWAYS(100000);
}

// 跟踪点数已增加的用户的地址
ghost address targetUser;

// ghost 映射，用于跟踪每个用户地址的点数
ghost mapping (address => mathint) ghostPoints {
    axiom forall address user. ghostPoints[user] >= 0 && ghostPoints[user] &lt;= max_uint24;
}

// hook 以验证存储读取是否与 ghost 状态匹配
hook Sload uint24 val allocations[KEY address user].points {
    require(require_uint24(ghostPoints[user]) == val);
}

// hook 以更新存储写入时的 ghost 状态
// 还跟踪第一个收到点数增加的用户
hook Sstore allocations[KEY address user].points uint24 val {
    // 仅当未设置且点数正在增加时才更新 targetUser
    targetUser = (targetUser == 0 && val > ghostPoints[user]) ? user : targetUser;
    ghostPoints[user] = val;
}

function initialize_constructor(address user1, address user2, address user3) {
    // 只有 user1、user2 和 user3 可以具有非零点数
    require(forall address user. user != user1 && user != user2 && user != user3 => ghostPoints[user] == 0);
    // 他们的点数总和必须等于总分配（100%）
    require(ghostPoints[user1] + ghostPoints[user2] + ghostPoints[user3] == TOTAL_POINTS_PCT());
}

function initialize_env(env e) {
    // 确保消息发送者是有效地址
    require(e.msg.sender != 0);
}

function initialize_users(address user1, address user2, address user3) {
    // 验证用户地址：
    // - 必须是非零地址
    require(user1 != 0 && user2 != 0 && user3 != 0);
    // - 必须是唯一地址
    require(user1 != user2 && user1 != user3 && user2 != user3);
    // 将 targetUser 初始化为零地址
    require(targetUser == 0);
}

// 验证总点数是否始终等于 TOTAL_POINTS_PCT (100%)
rule users_points_sum_eq_total_points(env e, address user1, address user2, address user3) {
    // 设置初始状态
    initialize_constructor(user1, user2, user3);
    initialize_env(e);
    initialize_users(user1, user2, user3);

    // 使用任何参数执行任何方法
    method f;
    calldataarg args;
    f(e, args);

    // 如果 targetUser 不是初始用户之一，则计算 targetUser 的点数
    mathint targetUserPoints = targetUser != user1 && targetUser != user2 && targetUser != user3 ? ghostPoints[targetUser] : 0;

    // 断言总点数保持恒定为 100%
    assert(ghostPoints[user1] + ghostPoints[user2] + ghostPoints[user3] + targetUserPoints == TOTAL_POINTS_PCT());

    // 所有其他地址必须具有零点数
    assert(forall address user. user != user1 && user != user2 && user != user3 && user != targetUser
        => ghostPoints[user] == 0
    );
}

示例 6 - 归属预先Claim Abuse

规范：VestingExt 合约包含与以前的 Vesting 合约相同的功能，以及一个附加功能，允许用户 preclaim 其 token 分配的一部分，允许用户在其归属期到期之前获得有限数量的 token。

在实现 fuzzer invariant 时，我验证了总 preclaimed 点数始终小于或等于最大可预先Claim的点数（这只是用户数量乘以每个用户的最大预先Claim点数）：

function property_total_preclaimed_lt_eq_max_preclaimable() public view returns(bool result我实现了与 [fuzzer](https://learnblockchain.cn/article/10147#heading-example-7-operator-registry-corruption) 相同的**不变性**，但在 Certora 的 [`rule`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/11-op-reg/certora.spec) 中更加优雅和简洁，再次展示了 Certora 领域特定形式验证语言的强大功能，尤其是在使用参数化规则时：

```solidity
// 给定两个已注册的 operator，不应该存在任何 f() 会破坏
// operator_id : operator_address 之间唯一关系的情况
rule operator_addresses_have_unique_ids(address opAddr1, address opAddr2) {
    // 在 `operatorAddressToId` 映射中强制执行唯一的地址
    require opAddr1 != opAddr2;

    uint128 op1AddrToId = currentContract.operatorAddressToId[opAddr1];
    uint128 op2AddrToId = currentContract.operatorAddressToId[opAddr2];

    // 在 `operatorAddressToId` 映射中强制执行有效且唯一的 operator_ids
    require op1AddrToId != op2AddrToId && op1AddrToId > 0 && op2AddrToId > 0;

    // 在 `operatorIdToAddress` 映射中强制执行匹配的地址
    require currentContract.operatorIdToAddress[op1AddrToId] == opAddr1 &&
            currentContract.operatorIdToAddress[op2AddrToId] == opAddr2;

    // 执行任何任意成功的交易 f()
    env e;
    method f;
    calldataarg args;
    f(e, args);

    // 验证是否没有交易会破坏
    // operator_id : operator_address 之间的唯一性属性
    assert currentContract.operatorIdToAddress[op1AddrToId] !=
           currentContract.operatorIdToAddress[op2AddrToId];
}

再次注意 require 语句的使用，指示 Certora 创建一个初始有效状态。

示例 8 - Liquidate Denial Of Service（清算拒绝服务）

规范：一个 LiquidateDos 合约允许交易者进入多个市场，并在每个市场中持有一个未平仓位。交易者也可以被清算：

在确定交易者是否可清算时，会考虑所有未平仓位
如果被清算，所有未平仓位都会为被清算的交易者平仓
清算不应因意外错误而失败

不幸的是，目前 Certora 不能用于意外的拒绝服务检查，因为 CVL 不返回 revert 的原因——它只提供 lastReverted 和 lastHasThrown，它们都是布尔值（如果使用 revert 操作码Hook，则提供 size）。Certora 在他们的 discord 中确认 “我们有一个在 prover 中实现此功能的计划”，因此一旦添加此功能，我们将进行更新。

示例 9 - Stability Pool Drain（稳定池耗尽）

规范：一个 StabilityPool 合约，它：

允许用户存入 debtToken，该 debtToken 用于在清算期间偿还不良债务
作为交换，debtToken 存款人从清算期间查获的抵押品代币中获得一部分作为奖励
包含相当复杂的逻辑来计算 debtToken 存款人应获得的奖励份额
必须始终保持偿付能力；该池应始终有足够的抵押品代币来支付欠 debtToken 存款人的奖励

使用 rule 结构，我将 fuzzer 中使用的不变性 转化为 Certora 能够求解的 “scenario”：

methods {
    // `envfree` 定义，用于调用没有显式 `env` 的函数
    function getDepositorCollateralGain(address) external returns (uint256) envfree;
}

// 稳定池存款人不能耗尽稳定池；稳定池应始终持有足够的**抵押品代币**
// 来支付欠存款人的奖励
rule stability_pool_solvent(address spDep1, address spDep2) {
    // 强制执行地址合理性检查
    require spDep1 != spDep2 &&
            spDep1 != currentContract &&
            spDep1 != currentContract.debtToken &&
            spDep1 != currentContract.collateralToken &&
            spDep2 != currentContract &&
            spDep2 != currentContract.debtToken &&
            spDep2 != currentContract.collateralToken;

    // 强制执行两个用户都没有 active deposits 或奖励
    require currentContract.accountDeposits[spDep1].amount     == 0 &&
            currentContract.accountDeposits[spDep1].timestamp  == 0 &&
            currentContract.depositSnapshots[spDep1].P         == 0 &&
            currentContract.depositSnapshots[spDep1].scale     == 0 &&
            currentContract.depositSnapshots[spDep1].epoch     == 0 &&
            currentContract.depositSums[spDep1]                == 0 &&
            currentContract.collateralGainsByDepositor[spDep1] == 0 &&
            currentContract.accountDeposits[spDep2].amount     == 0 &&
            currentContract.accountDeposits[spDep2].timestamp  == 0 &&
            currentContract.depositSnapshots[spDep2].P         == 0 &&
            currentContract.depositSnapshots[spDep2].scale     == 0 &&
            currentContract.depositSnapshots[spDep2].epoch     == 0 &&
            currentContract.depositSums[spDep2]                == 0 &&
            currentContract.collateralGainsByDepositor[spDep2] == 0;

    // 强制执行两个用户都有代币可以存入稳定池
    env e;
    uint256 user1DebtTokens = currentContract.debtToken.balanceOf(e, spDep1);
    uint256 user2DebtTokens = currentContract.debtToken.balanceOf(e, spDep2);
    require user1DebtTokens >= 1000000000000000000 && user2DebtTokens >= 1000000000000000000 &&
            user1DebtTokens == user2DebtTokens;

    // 两个用户将其 debt tokens 存入稳定池
    env e1;
    require e1.msg.sender == spDep1;
    provideToSP(e1, user1DebtTokens);
    env e2;
    require e2.msg.sender == spDep2;
    provideToSP(e2, user2DebtTokens);

    // 稳定池用于抵消清算产生的债务
    uint256 debtTokensToOffset = require_uint256(user1DebtTokens + user2DebtTokens);
    uint256 seizedCollateral = debtTokensToOffset; // 1:1
    env e3;
    registerLiquidation(e3, debtTokensToOffset, seizedCollateral);

    require(currentContract.collateralToken.balanceOf(e, currentContract) == seizedCollateral);

    // 强制执行每个用户应获得相同的奖励，因为他们存入了相同的
    uint256 rewardPerUser = getDepositorCollateralGain(spDep1);
    require rewardPerUser > 0;
    require rewardPerUser == getDepositorCollateralGain(spDep2);

    // 强制执行合约有足够的奖励代币来支付给两个用户
    require(currentContract.collateralToken.balanceOf(e, currentContract) >= require_uint256(rewardPerUser * 2));

    // 第一个用户提取他们的奖励
    env e4;
    require e4.msg.sender == spDep1;
    claimCollateralGains(e4);

    // 强制执行合约有足够的奖励代币来支付给第二个用户
    require(currentContract.collateralToken.balanceOf(e, currentContract) >= rewardPerUser);

    // 第一个用户执行任何任意成功的交易 f()
    env e5;
    require e5.msg.sender == spDep1;
    method f;
    calldataarg args;
    f(e5, args);

    // 第二个用户提取他们的奖励
    env e6;
    require e6.msg.sender == spDep2 &&
            e6.msg.value  == 0;
    claimCollateralGains@withrevert(e6);

    // 验证第一个用户无法做任何会导致
    // 第二个用户的提款 revert 的事情
    assert !lastReverted;
}

再次注意大量使用 require 语句来防止 Certora 通过生成无效状态来破坏断言。

示例 10 - Collateral Priority Corruption（抵押品优先级损坏）

规范：一个 Priority 合约，用于多抵押品借贷协议：

定义抵押品的清算优先级顺序
当发生清算时，风险最高的抵押品首先被清算，以便借款人剩余的抵押品篮子在清算后更加稳定
允许添加和删除抵押品；添加总是将新的抵押品放在优先级队列的末尾，而删除则保留现有的顺序，减去被删除的元素

在这里，我使用了与示例 #9 类似的方法，将 fuzzer 不变性 转换为一个rule，它描述了一个场景然后验证 Certora 能够打破的断言：

methods {
    // `envfree` 定义，用于调用没有显式 `env` 的函数
    function getCollateralAtPriority(uint8) external returns(uint8)   envfree;
    function containsCollateral(uint8)      external returns(bool)    envfree;
    function numCollateral()                external returns(uint256) envfree;
}

// 验证优先级队列顺序是否正确维护：
// - `addCollateral` 将新的 id 添加到队列的末尾
// - `removeCollateral` 保持现有顺序，减去被删除的 id
rule priority_order_correct() {
    // 需要没有初始抵押品以防止 HAVOC 破坏
    // EnumerableSet _positions -> _values 引用
    require numCollateral() == 0   && !containsCollateral(1) &&
            !containsCollateral(2) && !containsCollateral(3);

    // 使用抵押品 id 顺序设置初始状态：1,2,3，这确保
    // EnumerableSet _positions -> _values 引用是正确的
    env e1;
    addCollateral(e1, 1);
    addCollateral(e1, 2);
    addCollateral(e1, 3);

    // 健全性检查初始状态
    assert numCollateral() == 3  && containsCollateral(1) &&
           containsCollateral(2) && containsCollateral(3);

    // 健全性检查初始顺序；这也验证了
    // `addCollateral` 是否按预期工作
    assert getCollateralAtPriority(0) == 1 &&
           getCollateralAtPriority(1) == 2 &&
           getCollateralAtPriority(2) == 3;

    // 成功删除第一个 id 1
    removeCollateral(e1, 1);

    // 验证它已被删除，并且其他 id 仍然存在
    assert numCollateral() == 2  && !containsCollateral(1) &&
           containsCollateral(2) && containsCollateral(3);

    // 断言现有顺序 2,3 被保留，减去已删除的第一个 id 1
    assert getCollateralAtPriority(0) == 2 &&
           getCollateralAtPriority(1) == 3;
}

奖励 - Certora Foundry 插件

Certora 具有实验性的 Foundry 集成（文档，示例），允许通过 Certora 的形式验证运行 Foundry 无状态模糊测试。考虑包含 Chimera 风格 t() 断言的函数 test_RarelyFalse，如果 _rarelyFalse 返回 false，则该断言会失败：

uint256 constant private OFFSET = 1234;
uint256 constant private POW    = 80;
uint256 constant private LIMIT  = type(uint256).max - OFFSET;

// fuzzers 调用此函数
function test_RarelyFalse(uint256 n) external {
    // 输入前置条件
    n = between(n, 1, LIMIT);

    // 要打破的断言
    t(_rarelyFalse(n + OFFSET, POW), "Should not be false");
}

// 要测试的实际实现
function _rarelyFalse(uint256 n, uint256 e) private pure returns(bool) {
    if(n % 2**e == 0) return false;
    return true;
}

在撰写本文时，所有的 Fuzzer (Foundry/Echidna/Medusa) 都无法找到 _rarelyFalse 返回 false 的情况，导致 test_RarelyFalse 中的断言失败——但 Certora 可以非常快速地找到它，而无需编写任何额外的代码！首先创建配置文件 certora.conf，该文件除了通常的字段外，还有一个额外的可选 foundry_tests_mode 设置为 true：

{
  "files": [\
    "test/06-rarely-false/RarelyFalseCryticToFoundry.sol"\
  ],
  "verify": "RarelyFalseCryticToFoundry:test/06-rarely-false/certora.spec",
  "packages":[\
        "@chimera=lib/chimera/src",\
        "forge-std=lib/forge-std/src"\
    ],
  "foundry_tests_mode": true
}

然后 certora.spec 文件有这一行，它与测试完全无关：

use builtin rule verifyFoundryFuzzTests;

这个简单的设置允许使用 Certora 对 Foundry 无状态模糊测试进行形式验证！

可能的改进

由于 Certora 已经创建了自己的领域特定语言，如果它包含一些 “syntactic sugar（语法糖）”，使常见模式更容易实现且不易出错，那就太好了。

一种常见的模式是使用 ghost variable（幽灵变量） 来跟踪映射中所有值的总和；这在示例 5 的第二个解决方案中使用。目前，这种模式实现起来相当繁琐且容易出错——如果提供一些语法糖，将其变成像这样的一行代码，那就更好了：

// 对映射中的所有值求和
ghost mathint sumOfPoints = always_sum(currentContract.allocations.points);

// 对给定的一组键（这里是地址）的映射中的值求和
ghost mathint sumOfPoints = always_sum(currentContract.balances, users);

另一个潜在的改进是让 certoraRun 自动从 Hardhat/Foundry 配置文件中读取库路径，这样就不需要在 .conf 文件中复制这些路径。