基于 Recon 与 Medusa 构建不变量测试

概述

不变量测试是目前最高效的智能合约测试方法之一。在我较早编写的 Foundry 高级测试: Fuzz、Invariant与形式化证明 曾介绍过基于 Foundry 的不变量测试方法，但该文已经编写于 2 年前。在过去 2 年中，有一系列新的工具产生，比如 medusa 工具，并且出现了专业的不变量测试服务商，比如 Recon。

本文将基于 Recon 编写的 create-chimera-app 和 Medusa 工具介绍不变量测试的方法。和过去的文章一致，本文依旧会使用案例演示的方法，本文主要使用的案例是 Damn Vulnerable DeFi，该网站内包含一些 CTF 题目，我们会使用不变量测试解决这些问题。事实上， Solidity Fuzzing Challenge 已经尝试使用不同的不变量测试工具解决这些问题了。

Update: 在最新一次更新后，本文可能不会使用 Damn Vulnerable DeFi 作为案例，本文认为 How Echidna inflated 100s of Millions in Voting Power: Writing and Breaking Properties 可能是一个更优秀的案例，此处仍需一些评估

不变量测试

在本文的开始，我们首先简单讨论一下不变量测试的基础含义。我们可以认为不变量测试是一种高级的集成测试手段，我们会生成一系列随机调用对合约进行调用，最后检查合约内的某些不变量是否保持。那么什么是合约不变量( invariants，在很多情况下，合约不变量也被称为属性 property，一般两者都会被混用)呢？简单的案例包括:

1. ERC20 供应量 = 所有用户的余额 = 铸造数量 - 销毁数量
2. AMM 系统内存在 x * y = k 的不变量函数
3. 借贷协议中系统的利息随着时间会逐渐增加

当然，实际上在智能合约最初设计时，我们就已经有意无意使用了不变量的概念，此处笔者建议开发者在最初讨论系统设计时就考虑不变量问题，并将所有设计过程中考虑的不变量归纳到表格内部，等待最终进行不变量测试时使用。当然，在开发过程中，开发者也可以随时关注编写的代码是否打破了不变量。不变量是极其重要的智能合约设计规则，以至于 Trail of Bits 曾撰文呼吁智能合约工程师使用不变量驱动开发。本节中的部分内容就来自 Trail of Bits 的这篇呼吁不变量驱动开发的文章 The call for invariant-driven development。Trail of Bits 也开源了一份常见 ERC 的 不变量测试列表。值得注意的，不变量测试不一定只检测 x = y 这种完全相等性测试，我们也可以设置 x < y 这种不等测试，在很多情况下，进行不等测试是更加有效的。

对于不变量该如何更加正确的识别，Dacian 在 Writing Multi-Fuzzer Invariant Tests Using Chimera 指出我们可以将智能合约的生命周期视为三个阶段:

1. 构建和初始化
2. 正常执行
3. 结束状态(可选)

每一个阶段都可能存在不变量。比如 AMM 在正常执行时，假如不存在手续费，那么一定会存在 x * y = k 的结果。或者比如 ERC4626 内一个用户存款后立即取款，当金库内的资金没有增加时，该用户应该可以将所有资产取出，假如不可以，那么就代表 ERC4626 金库受到了攻击，比如经典的 Inflation attack。

最近知名安全测试工程师 Rappie 在 推文 内指出了自己设计不变量的方法。首先，我们可以分析一些简单的不变量，比如“所有余额的总量等于当前代币的总供应量”，这种简单的不变量就可以帮助我们发现一系列问题。进一步深入的不变量需要安全测试工程师与开发团队进行交流，了解开发团队最担心的问题有哪些，然后根据这些开发者所担忧的问题进一步构造不变量测试。

Recon 的工程师 GalloDaSballo 曾在 Push & Pop #59 - Alex - Recon Extension 和 How Echidna inflated 100s of Millions in Voting Power: Writing and Breaking Properties 给出了自己对于不变量测试的一些定义。该工程师将不变量测试分为以下几种类型：

1. Global Properties 全局不变量，一个最简单的例子就是合约的偿付能力问题，以质押奖励分配为例，合约内部跟踪的所有待分配代币总量应该与当前合约持有的代币数量一致，
2. State Changing Properties 状态变化不变量，交易会对合约状态进行修改，而状态变化不变量是用来确定状态修改是否与预期一致，比如用户向合约存入资产，那么用户的余额应该会增加与存入资产等量的数量
3. Doomsday Properties 这是一种最特殊的不变量，是指在当前合约状态下进行一些极端操作，比如借贷合约内所有的用户都进行提款操作

GalloDaSballo 强调了在进行不变量测试中使用 数学归纳法 的重要。数学上的归纳法是指我们只需要证明当 \(n = 0\) 时命题成立，同时证明在 \(n = k\) 时，\(n = k + 1\) 情况下命题也是成立的，如此我们就证明了命题的正确性。不变量测试中很多验证的底层思想都类似数学归纳法。

关于不变量测试，业界也存在了很多实战类型文章，读者可以按需阅读:

1. Find Highs Before External Auditors Using Invariant Fuzz Testing
2. Implementing Your First Smart Contract Invariants: A Practical Guide

当然，读者也可以直接阅读本文中的内容，本文的内容会较为连贯，阅读完成本文后也可以使用本文提供的技术框架重新实现上述几篇文章内的案例。

基础工具

Medusa 是一个使用 go 语言开发的基于 go-ethereum 的不变量测试工具， Solidity Fuzzing Challenge 显示该测试工具具有较高的性能和良好的调用顺序生成器，可以快速寻找到协议代码内打破不变量的情况。假如读者对 Medusa 的性能等感兴趣，可以尝试阅读 Medusa 开发商 Trail of Bits 编写的博客 Unleashing Medusa: Fast and scalable smart contract fuzzing。

对于 medusa 测试工具的安装，读者可以自行参考 文档。但是对于 MacOS 用户而言，可以直接使用以下命令即可:

brew install medusa

而 create-chimera-app 是一个由 Fuzz 服务商 Recon 编写的不变量测试框架，该框架最有趣的是同时支持 Foundry / Medusa / echidna 等多个不变量测试工具。但在本文中，我们主要使用 Foundry 和 Medusa 两个工具。该框架倡导开发者首先使用 Foundry 内的各种工具完成一些调用队列的正确性测试，保证特定的调用队列可以正常执行，然后使用 Medusa 随机生成调用队列，假如 Medusa 发现特殊情况，比如打破了不变量，那么我们可以将该出现问题的调用队列转移到 Foundry 工具内进行 Debug。在具体表现上， create-chimera-app 内存在 CryticToFoundry 合约，该合约就是用来存放一些单纯的 Foundry 单元测试来辅助 Medusa 工作。

需要注意的，medusa 在 slither 辅助下可以更好的工作，所以此处建议读者使用以下命令安装 slither 工具。更加具体的说， slither 会在 medusa 运行前对智能合约内内容进行提取，提取后的数据可以进一步辅助 medusa 进行测试。

brew install slither-analyzer

另一个较为重要的工具是 recon-extension。该工具为开发者提供了一键生成测试脚手架的功能，此处建议读者安装。笔者为了避免 recon-extension 对日常开发环境的影响使用了 VSCode Profiles 的特性，该特性可以使得开发者构建出 VSCode 配置不同的几个工作空间，笔者专门为 recon-extension 创建了一个专门用于不变量测试的工作空间。

Medusa 的基础原理

在介绍具体的不变量测试前，我们最好对 Medusa 等不变量测试工具有一定了解。不变量测试工具的基础原理是生成一系列的调用序列然后按照调用序列直接对一系列目标函数进行调用。作为合约工程师，我们一般会构建一个被称为 TargetFunctions 的合约，该合约内部包含所有我们认为需要被 medusa 调用的函数。以 create-chimera-app 框架为例，该框架内的 CryticTester 合约实际上就是 medusa 调用序列所调用的合约，该合约的具体内容如下:

import {CryticAsserts} from "@chimera/CryticAsserts.sol";

import {TargetFunctions} from "./TargetFunctions.sol";

// echidna . --contract CryticTester --config echidna.yaml --format text --workers 16 --test-limit 1000000
// medusa fuzz
contract CryticTester is TargetFunctions, CryticAsserts {
    constructor() payable {
        setup();
    }
}

此处的 TargetFunctions 已经在上文有所提及。与大家认知不同的是，不变量测试其实也是随机生成的调用函数中的一环，只是不变量测试一定会在随机生成的调用队列内出现。还是以 create-chimera-app 框架为例，我们可以在 AdminTargets 合约(该合约是 TargetFunctions 的父合约， TargetFunctions 与该合约存在继承关系)内找到如下定义:

abstract contract AdminTargets is
    BaseTargetFunctions,
    Properties
{
    /// CUSTOM TARGET FUNCTIONS - Add your own target functions here ///

    /// AUTO GENERATED TARGET FUNCTIONS - WARNING: DO NOT DELETE OR MODIFY THIS LINE ///
}

此处的 Properties 就是包含不变量测试的合约，所以 TargetFunctions 内部已经包含了不变量测试的有关代码。当我们已知 Medusa 如何判断哪些函数需要被调用后，我们会希望进一步了解这些测试序列如何生成？这部分内容在 medusa fuzzing lifecycle 已有部分介绍，非常建议读者阅读这部分文档。

在此处，我们先看一段来自 Medusa 的配置文件 medusa.json 内的内容:

{
  "callSequenceLength": 100,
  "corpusDirectory": "medusa",
  "targetContracts": [\
    "CryticTester"\
  ],
}

此处的内容中 targetContracts 其实就是 Medusa 所需要随机调用的合约，而 callSequenceLength 代表每一次生成随机调用序列的长度，所以不变量测试其实并不是进行大量调用后再判断不变量是否被满足，而是存在很多随机调用序列执行，但每一个调用序列执行完成后，测试工具会擦除当前 EVM 的状态。

对于随机序列的生成，Medusa 使用了两种方式:

1. 根据目标函数所需要的参数类型直接随机生成随机调用的 calldata，但这种模式可能会产生问题，即大量的调用都会因为各种原因 revert 导致生成的大部分随机调用无效
2. 为了避免大量调用无效，Medusa 使用了 corpus 概念。在理解该概念之前，我们需要理解测试覆盖率引导测试数据生成。此处的测试覆盖率引导指 Medusa 内部会跟踪当前生成的 calldata 所覆盖的字节码范围，并追求测试覆盖率最大化的目标。为了实现此目标，Medusa 每发现一个会增加测试覆盖率的调用序列就会将其记录到 corpus 内部，并且根据 corpus 内部的调用序列进行微调已获得更好的覆盖范围

corpus 是 Medusa 最优秀的特性，我建议读者可以在模糊测试长时间没有覆盖率提升时对 corpus 内部的调用队列进行观察。读者可以在 medusa/call_sequences 文件夹内部找到很多 JSON 文件，每一个 JSON 文件内都包含一个 Medusa 找到的 corpus 队列。 corpus 队列是一个由 call 数据构成的列表:

 {
  "call": {
   "from": "0x7fa9385be102ac3eac297483dd6233d62b3e1496",
   "to": "0x7d8cb8f412b3ee9ac79558791333f41d2b1ccdac",
   "nonce": 19,
   "value": "0x0",
   "gasLimit": 12500000,
   "gasPrice": "0x1",
   "gasFeeCap": "0x0",
   "gasTipCap": "0x0",
   "data": "0x280203d7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe000000000000000000000000965467f65080360c1683ecb814d0b318e6cc733d000000000000000000000000000000000000000000000000000000000000008000000000000000000000000000000000000000000000000000000000000000035453540000000000000000000000000000000000000000000000000000000000",
   "dataAbiValues": {
    "methodSignature": "morpho_supply(uint256,uint256,address,bytes)",
    "inputValues": [\
     "115792089237316195423570985008687907853269984665640564039457584007913129639934",\
     "115792089237316195423570985008687907853269984665640564039457584007913129639934",\
     "0x965467f65080360c1683ecb814D0B318e6cC733d",\
     "545354"\
    ]
   },
   "AccessList": null,
   "SkipAccountChecks": true
  },
  "blockNumberDelay": 0,
  "blockTimestampDelay": 214979
 }

以下伪代码显示了 Medusa 的基础工作原理:

## Generate a new call sequence or mutate one from the corpus
sequence = generator.NewCallSequence()

## Iteratively execute each call in the call sequence
for i < len(sequence) {
    # Retrieve the i-th element in the sequence
    tx = sequence[i]

    # Run the transaction on the blockchain and retrieve the result
    result = blockchain.executeTransaction(tx)

    # Update coverage
    increasedCoverage = coverageTracker.updateCoverage()

    # If coverage increased, add sequence[:i+1] to the corpus
    if increasedCoveraged {
        corpus.addCallSequence(tx[:i+1])
    }

    # Check for invariant failures
    encounteredFailure = tester.checkForInvariantFailures(result)

    # Let user know we had a failing test case
    if encounteredFailure {
        reportFailedTestCase()
    }
}

从 Medusa 生成随机序列的方法可以看出，假如 Medusa 生成了一些可能导致 revert 的序列，那么 Medusa 就会调整自己的随机序列，并尽可能减少 revert 的发生。Meudsa 将定义为 coverage-guided fuzzer。所谓的 coverage-guided fuzzer 指模糊测试程序使用一系列方法目标是最大限度地扩大其测试的系统覆盖率。

可能有读者希望利用某种方法操作调用序列随机性，比如我们希望调用序列内一定需要包括 repay 和 liquidate 函数，此处我们将使用到在 Medusa 文档内没有提到的 Shrink 特性 。该特性实际位于上文伪代码中的 checkForInvariantFailures 函数内部。该特性会在属性测试失败后被触发，Medusa 就会修改之前的调用队列，查找可移除的冗余调用并且验证修改后的调用队列满足 属性测试要求，所以开发者可以构建一些特殊的属性测试，这些测试并不检查不变量而是用于检查调用序列是否调用了某一个函数。以上文的 repay 和 liquidate 函数必须被调用为例，我们可以在目标函数内构造如下调用:

function morpho_liquidate(address borrower, uint256 seizedAssets, uint256 repaidShares, bytes memory data)
    public
    updateGhosts
    asActor
{
    morpho.liquidate(marketParams, borrower, seizedAssets, repaidShares, data);

    hasLiquidated = true;
}

function morpho_repay(uint256 assets, uint256 shares, address onBehalf, bytes memory data)
    public
    updateGhosts
    asActor
{
    morpho.repay(marketParams, assets, shares, onBehalf, data);

    hasRepaid = true;
}

上述代码中的 hasLiquidated 和 hasRepaid 作为状态变量标识函数是否被调用，然后我们可以在属性测试内增加以下属性测试:

function canary_hasDoneRepay() public {
    t(!hasRepaid, "canary_hasDoneRepay");
}

function canary_hasDoneLiquidate() public {
    t(!hasLiquidated, "canary_hasDoneLiquidate");
}

此时，假如 Medusa 没有对 morpho_repay 和 morpho_liquidate 函数进行调用，那么该序列中的调用到 canary_hasDoneRepay 和 canary_hasDoneLiquidate 就会触发属性测试失败，此时 Medusa 会使用 Shrink 机制优化调用序列。

假如读者对 shrink 的细节感兴趣，可以阅读此处的 源代码

我们讨论另一个问题，假如读者曾经使用过 Foundry 的标准库进行测试，会发现 Foundry 为用户提供了很多 cheatcode 用于修改各种区块状态或者交易上下文，比如我们可以使用 startPrank 修改之后 call 调用的 msg.sender。但是 Medusa 等工具支持这些 cheatcode 吗？此处我们就要介绍一个被称为 HEVM 工具，该工具提供了最早期的 cheatcode 并以此构造了测试工具。后续开发的 Foundry 等工具基本都实现了 HEVM 内定义的 cheatcode，而 Medusa 等现代测试工具也不例外。所以理论上只要使用 HEVM 内的 cheatcode 就可以实现测试的最大兼容性。实际上， create-chimera-app 框架的核心代码也就是构造基于 HEVM 内的 cheatcode 构造不同测试的通用代码。

最后，我们讨论最后一个问题，不变量测试工具如何判断测试失败？在 Foundry 测试中，我们一旦使用 assertEq 等判断函数，这些函数本质上调用了 VM_ADDRESS 合约。我们可以认为该合约是一个预汇编合约，所有对该合约的调用会被转移到 Foundry 内的 Rust 程序组件处理。而 Medusa 等不变量测试使用了 solidity 原生的 assert 方法，我们可以在 chimera 内看到如下代码:

function gt(uint256 a, uint256 b, string memory reason) internal virtual override {
    if (!(a > b)) {
        emit Log(reason);
        assert(false);
    }
}

此处 assert 会释放一些特殊的 revert 报错信息，Medusa 通过捕获这些特殊的报错信息确定测试是否失败。注意，这些测试报错与我们在合约内定义的 revert 并不完全一致，Medusa 可以通过这种不一致分别测试是被 assert 中断还是被正常中断。Medusa 内的相关代码如下:

// checkAssertionFailures checks the results of the last call for assertion failures.
// Returns the method ID, a boolean indicating if an assertion test failed, or an error if one occurs.
func (t *AssertionTestCaseProvider) checkAssertionFailures(callSequence calls.CallSequence) (*contracts.ContractMethodID, bool, error) {
    // If we have an empty call sequence, we cannot have an assertion failure
    if len(callSequence) == 0 {
        return nil, false, nil
    }

    // Obtain the contract and method from the last call made in our sequence
    lastCall := callSequence[len(callSequence)-1]
    lastCallMethod, err := lastCall.Method()
    if err != nil {
        return nil, false, err
    }
    methodId := contracts.GetContractMethodID(lastCall.Contract, lastCallMethod)

    // Check if we encountered an enabled panic code.
    // Try to unpack our error and return data for a panic code and verify that that panic code should be treated as a failing case.
    // Solidity >0.8.0 introduced asserts failing as reverts but with special return data. But we indicate we also
    // want to be backwards compatible with older Solidity which simply hit an invalid opcode and did not actually
    // have a panic code.
    lastExecutionResult := lastCall.ChainReference.MessageResults().ExecutionResult
    panicCode := abiutils.GetSolidityPanicCode(lastExecutionResult.Err, lastExecutionResult.ReturnData, true)
    failure := false
    if panicCode != nil {
        failure = encounteredAssertionFailure(panicCode.Uint64(), t.fuzzer.config.Fuzzing.Testing.AssertionTesting.PanicCodeConfig)
    }

    return &methodId, failure, nil
}

脚手架内容

本节主要介绍 create-chimera-app 框架的具体架构以及不同的文件具体含义。 create-chimera-app 的核心文件都位于 test/recon 文件夹内，此处笔者对 RewardsManager-Invariants 为例介绍。我们可以使用 git clone https://github.com/GalloDaSballo/RewardsManager-Invariants.git 将该项目 clone 到本地。然后直接使用 rm -rf test/recon 删除掉原有的测试文件。接下来，我们可以使用 recon-extension 插件初始化不变量测试项目，只需要选择目标合约 RewardsManager 然后点击 Scaffold 即可。

等待插件安装依赖并生成一系列脚手架文件。最后，我们可以在 test/recon 文件夹内找到以下内容:

.
├── BeforeAfter.sol
├── CryticTester.sol
├── CryticToFoundry.sol
├── Properties.sol
├── Setup.sol
├── TargetFunctions.sol
└── targets
    ├── AdminTargets.sol
    ├── DoomsdayTargets.sol
    ├── ManagersTargets.sol
    └── RewardsManagerTargets.sol

看上去 Recon 扩展生成了一系列复杂的脚手架代码，似乎很难理解。读者应该根据上文介绍的 Medusa 的基础原理对这些合约进行理解。这些合约本质上就是提供了 Medusa 需要随机调用的函数和属性测试的具体内容。

我们可以首先阅读 Setup 合约，该合约与 foundry 测试中的 setUp 函数作用一致，用来配置不变量测试开始前的基础合约环境。我们一般会在此合约内完成测试目标合约的部署以及与测试有关的一些其他配置，比如为借贷协议配置预言机等。我们可以看到 SetUp.sol 内部包含以下内容：

abstract contract Setup is BaseSetup, ActorManager, AssetManager, Utils {
    RewardsManager rewardsManager;

    /// === Setup === ///
    /// This contains all calls to be performed in the tester constructor, both for Echidna and Foundry
    function setup() internal virtual override {
        rewardsManager = new RewardsManager(); // TODO: Add parameters here
    }

    /// === MODIFIERS === ///
    /// Prank admin and actor

    modifier asAdmin {
        vm.prank(address(this));
        _;
    }

    modifier asActor {
        vm.prank(address(_getActor()));
        _;
    }
}

其中 setup 函数内，我们可以进行合约部署等。剩下的 asAdmin 和 asActor 是系统生成的用于修改调用者的修饰器，该修饰器会在 TargetFunctions 中使用，其用途是在不变量测试过程中修改调用目标函数的请求者地址。我们可以看到 asAdmin 修饰符会将调用者修改为当前的 SetUp 合约，而 asActor 则会调用 _getActor 函数在已有的调用者序列内随机抽取调用者来调用目标合约。

ActorManager 合约内部对 _getActor 进行了实现，实际上 ActorManager 模块的作用就是提供了一系列辅助函数用于调整不变量测试过程中随机调用目标函数时所使用的调用者地址，我们可以通过 _addActor 函数增加调用者序列内的调用者地址，使用 _switchActor 修改调用者。但是需要注意的，我们一般会直接将 _switchActor 函数也作为不变量测试过程中可以被调用的函数，不变量测试工具为自动调用该函数修改 actor 地址

TargetFunctions 文件内定义了在不变量测试中，fuzz 工具会生成的随机调用目标函数，该合约的代码如下：

abstract contract TargetFunctions is
    AdminTargets,
    DoomsdayTargets,
    ManagersTargets,
    RewardsManagerTargets
{
    /// CUSTOM TARGET FUNCTIONS - Add your own target functions here ///

    /// AUTO GENERATED TARGET FUNCTIONS - WARNING: DO NOT DELETE OR MODIFY THIS LINE ///
}

我们可以看到该合约其实是一个空合约，但继承了 targets 文件夹内的四个合约。我们会在后文依次介绍每一个合约内的具体内容。我们首先分析 RewardsManagerTargets 合约，该合约部分代码如下：

function rewardsManager_accrueUser(uint256 epochId, address vault, address user) public asActor {
    rewardsManager.accrueUser(epochId, vault, user);
}

function rewardsManager_accrueVault(uint256 epochId, address vault) public asActor {
    rewardsManager.accrueVault(epochId, vault);
}

事实上，该合约其实就是根据 rewardsManager 合约的 ABI 生成的， RewardsManagerTargets 内部包含所有在 rewardsManager 合约内定义的可以在外部被调用的函数。该合约也是我们未来修改加工的基础，有了 RewardsManagerTargets 合约，我们可以在上面编写其他函数。

ManagersTargets 合约内主要包含 asset 和 actor 管理。包含以下几个函数:

1. switchActor 更换当前调用过程中的 actor，该函数被调用后会影响后续 asActor 修饰符内的 _getActor 函数返回值
2. switch_asset 在资产列表内获取一个资产地址并更换随后所有调用过程中使用的资产
3. add_new_asset 向资产列表内增加资产
4. asset_approve 和 asset_mint 顾名思义分别用于资产的授权和铸造

简单来说，我们可以将 ManagersTargets 视为一个维护随机调用过程中 actor 和 asset 的上下文工具，我们可以通过调用内部的函数实现 actor 的增加和切换，以及资产的增加、切换、铸造和授权等功能。

AdminTargets 的作用非常简单，该合约内主要存储那些 asAdmin 修饰符修饰的函数，比如那些待测试合约内只能由 owner 调用的函数。而 DoomsdayTargets 合约内的主要存储那些上文介绍的符合 Doomsday Properties 的测试。我们可以看到该合约内存在以下修饰符:

modifier stateless() {
    _;
    revert("stateless");
}

这是因为 Doomsday Properties 测试都是测试极端情况下的系统表现，所以这些属性测试一旦被调用就会大幅度干扰合约正常的状态，这会导致其他测试无法正常执行。所以理论上所有的 Doomsday Properties 测试都应该是 stateless，该函数被调用但是调用会被 revert。在上文中，我们提及此处的 revert("stateless") 和 assert 导致的 revert 并不一致，所以我们实际上可以在 Doomsday 测试内编写不变量测试，而执行完成后的 revert("stateless"); 并不会影响不变量测试。

BeforeAfter 和 Properties 都是直接为不变量测试服务的，我们会在后文介绍不变量编写时详细介绍，此处我们只需要知道 BeforeAfter 内包含 updateGhosts 函数，可以更新一些 Ghosts 变量，这些变量主要在调用序列中跟踪一些状态，值得注意的，我们不能在 updateGhosts 内部编写可能发生 revert 的函数，因为这些函数可能导致 updateGhosts 失败进一步导致逻辑代码调用失败。这种失败会导致覆盖范围在异常降低，甚至导致某些情况始终无法覆盖。 Properties 是核心编写不变量测试的合约。

最后，我们介绍一些不太重要的其他合约:

1. CryticTester Medusa \ Echidna 测试工具等入口合约，此处的 Crytic 其实就是 Medusa \ Echidna 工具的开发商
2. CryticToFoundry 用于存储一些在 Foundry 内执行的测试，假如 Medusa 等工具在不变量测试内出现了报错，我们可以将报错信息转化为 Foundry 测试代码放到 CryticToFoundry 内执行，简单来说，我们可以在这个合约内使用 Foundry 编写一些临时的调用代码

• 本文转载自： hackmd.io/evm0Y5w7RF2MhS... , 如有侵权请联系管理员删除。