介绍Recon：简化的不变性测试和模糊测试

allthingsfuzzy
发布于 2024-02-26 23:30
阅读 34

本文介绍了Recon工具的使用，该工具能自动化生成Solidity项目的无变体测试。作者通过示例展示了如何使用Recon创建Uniswap V3的测试套件，并验证特性以检测智能合约中的潜在漏洞。文章详细阐述了项目设置过程、各个合约的功能以及如何运行模糊测试。整体上，该文本为开发人员和审计人员提供了很好的工具使用指南。

Feb 24, 2024

![](https://img.learnblockchain.cn/2025/03/08/ff80d2e4-bb52-4c34-b523-a7ed4dada696_2138x1000.png)

## 什么是 Recon？

[Recon](https://getrecon.xyz/) 是一款加速编写不变性测试过程的工具。它可以连接到任何开源的 Solidity 项目，并自动生成用于创建 Echidna、Medusa 和 Foundry 的不变性测试的骨架代码，只需几次点击。

开发者和审计员可以不再花费数小时来设置测试套件，而是将精力集中在创建可能发现其系统中漏洞的相关属性上。

## 它是如何工作的

在本次测试工具演示中，我们将使用 Uniswap v3 仓库，因为大多数审计员和开发者都熟悉这个代码库。

在发布之前，Uniswap V3 经过了 [Trail of Bits](https://github.com/Uniswap/v3-core/blob/main/audits/tob/audit.pdf) 的审计，他们扩展了现有的 Echidna 测试套件并定义了应该在整个系统中保持的属性。在这个示例中我们要关注的属性是：

1. 如果调用 swap 不改变 `sqrtPriceX96`，流动性将不会改变（Property-17）

我们将看到如何在几个步骤中使用 Recon 创建一个新的测试套件，并开始测试这个属性。

下面示例创建的仓库可在 [这里](https://github.com/nican0r/recon-uniswapv3/tree/main) 找到。

### 项目设置

![](https://img.learnblockchain.cn/2025/03/08/26ecb08e-8833-4b57-bb95-49d1341bc29f_1208x1276.png)

点击“开始工作”将启动 Recon 云服务上的构建任务，该任务将返回项目中的所有合约，并能够选择添加到测试工具中的功能。

由于在本演示中，我们只会测试与 `Pool` 合约函数和 `TestERC20` 状态变量相关的属性，因此我们不需要从目标合约中选择任何函数。如果我们要创建 Echidna [布尔属性测试](https://github.com/crytic/building-secure-contracts/blob/master/program-analysis/echidna/basic/testing-modes.md#boolean-properties)以对特定函数的输入值进行模糊测试，我们将在此选择感兴趣的函数，并在 `Properties` 合约中定义我们的属性。在我们的使用案例中，我们保留 `mint` 和 `swap` 函数，以防将来决定从“构建处理程序”页面添加布尔属性测试，并取消选择（以红色标记）所有不感兴趣的函数：

![](https://img.learnblockchain.cn/2025/03/08/F02e9fa93-5e2c-42d1-8ab4-7f515c668c04_1626x330.png)

在“前后跟踪器”标签中，我们可以选择在 Pool 合约中要跟踪的状态变量，以便进行断言，这类似于 Certora 或 Foundry 教程中的“幽灵变量”。

在我们的案例中，我们将仅使用来自 `TestERC20` 合约的 `balanceOf` 和 `UniswapV3Pool` 中的 `feeGrowthGlobal0X128`、`feeGrowthGlobal1X128`、`liquidity`、`slot0` 和 `ticks`，因为这些是我们需要证明流动性属性的全部内容：

![](https://img.learnblockchain.cn/2025/03/08/F64e925e4-bc05-4ca6-a595-8a4178fe6940_2040x968.png)

一旦我们选择了这些变量，我们可以看到“结果页面”，在这里我们可以访问所有测试工具的文件：

#### TargetFunctions.sol

![](https://img.learnblockchain.cn/2025/03/08/Fd05309af-e656-46c6-8e10-548c9ec104bc_2164x910.png)

此文件为我们感兴趣的合约函数提供了一个入口点，Echidna/Medusa/Foundry 在运行布尔属性测试时会调用这些函数，并且是我们可以定义断言测试的地方。

#### BeforeAfter.sol

![](https://img.learnblockchain.cn/2025/03/08/f9a47c52-751c-4198-92fd-736f39adafa6_1618x1396.png)

此文件提供了合约变量的幽灵副本，这些副本存储在一个结构中，并通过调用 `__before` 和 `__after` 函数进行更新。它们简化了访问合约中状态变量值的过程，使其更容易通过存储幽灵变量的 `_before` 和 `_after` 结构进行访问。

#### Setup.sol

Setup 合约简单地用于部署系统所需的所有合约。由于每个系统的部署可能是特定的，因此需要手动修复，这就是为什么默认值是对测试套件实施者的 TODO。在这个示例中，由于与 `UniswapVPool` 的一些奇怪之处，我们在此没有实例化它，而是使用 `_init` 函数。

#### CryticToFoundry.sol

此合约用于创建 Foundry 的单元测试，用于检测 Echidna/Medusa/Foundry 模糊测试运行的失败案例。这对于集成到开发流水线中非常有用，因为它可以让你看到更改是否已解决先前发现的失败案例，或者是否会产生新的违规行为。

#### CryticTester.sol

![](https://img.learnblockchain.cn/2025/03/08/2F0a2e3967-1fde-409f-ae65-b1198778e1ba_984x312.png)

这是进入 Echidna 和 Medusa 的主要入口，以调用模糊测试合约。

#### Properties.sol

![](https://img.learnblockchain.cn/2025/03/08/2Fc714e6df-8f2f-414b-8419-42f7cd94afd1_842x378.png)

在这里，你将编写需要在感兴趣的合约上测试的属性。

#### [medusa.json](https://github.com/nican0r/recon-uniswapv3/blob/main/medusa.json) 和 [echidna.yaml](https://github.com/nican0r/recon-uniswapv3/blob/main/echidna.yaml)

这些只是用于配置 Echidna 和 Medusa 的配置文件，用于调整运行测试期间模糊测试器的设置。

### 运行模糊测试器

#### 设置

Recon 默认配置 Echidna 以对函数名以 `invariant_` 开头的布尔属性测试，而不是标准的 `echidna_` 前缀。

我们将使用 Trail of Bits 团队为上述选择的属性创建的断言测试，并进行了修改，以便它们可以与 Recon 创建的工具正常工作。由于这些测试是断言测试，因此需要调用合约函数以验证特定状态，因此我们将它们定义在 `TargetFunctions` 合约中，而不是在 `Properties` 中，我们可以使用任何前缀来命名，因此使用 `test_`。

**注意**：附带的仓库已包含以下设置步骤，但如果你使用自己的仓库，你需要遵循这些步骤以添加 Recon 工具。

**对于不使用 Foundry 的项目**：由于 Uniswap V3 仓库未实现 Foundry，因此我们首先需要通过 `forge install` 来添加它。这使我们能够使用 Foundry 的增强调试工具来调试问题，并为在模糊测试活动过程中可能发现的任何失败案例创建 Foundry 测试。

在 Recon 的“结果页面”中，你将有机会下载从创建工具生成的文件，这些文件应添加到 Foundry 创建的 tests/ 目录中。

我们还需要通过 `forge install Recon-Fuzz/chimera` 来添加 Chimera 依赖项，帮助配置我们的项目以使用 Recon 工具。

然后我们在 `foundry.toml` 文件中将 Chimera 添加到我们的重映射中，并添加一些配置以确保 CryticCompiler 与 Uniswap 使用的 solc 编译器版本兼容：

```
[profile.default]
remappings = [\
    'forge-std/=lib/forge-std/src/',\
    '@chimera/=lib/chimera/src/'\
]
solc = "0.7.6"
evm_version = "istanbul"
```

#### Swap 属性测试

对于我们想要测试的属性：

- 如果调用 swap 不改变 `sqrtPriceX96`，流动性将不会改变

我们在 `Setup` 合约中定义了一个检查此属性的断言：

```
function check_swap_invariants(
        int24 tick_bfre,
        int24 tick_aftr,
        uint128 liq_bfre,
        uint128 liq_aftr,
        uint256 bal_sell_bfre,
        uint256 bal_sell_aftr,
        uint256 bal_buy_bfre,
        uint256 bal_buy_aftr,
        uint256 feegrowth_sell_bfre,
        uint256 feegrowth_sell_aftr,
        uint256 feegrowth_buy_bfre,
        uint256 feegrowth_buy_aftr
    ) internal {
        // 属性 #17
        if (tick_bfre == tick_aftr) {
            assert(liq_bfre == liq_aftr);
        }
    }
```

该断言将在 `TargetFunctions` 中的以下测试函数中进行评估：`test_swap_exactIn_zeroForOne`、`test_swap_exactIn_oneForZero`、`test_swap_exactOut_zeroForOne` 和 `test_swap_exactOut_oneForZero`。

我们的测试使用 `BeforeAfter` 合约提供的前后幽灵变量来检查系统的状态，并确保属性没有被违反：

```
        __before();
        swapper.doSwap(true, _amountSpecified, sqrtPriceLimitX96);
        __after();

int24 beforeCurrentTick = _before.uniswapV3Pool_currentTick;
        int24 afterCurrentTick = _after.uniswapV3Pool_currentTick;

check_swap_invariants(
            beforeCurrentTick,
            afterCurrentTick,
            _before.uniswapV3Pool_liquidity,
            _after.uniswapV3Pool_liquidity,
            _before.testERC20_balanceOfToken0,
            _after.testERC20_balanceOfToken0,
            _before.testERC20_balanceOfToken1,
            _after.testERC20_balanceOfToken1,
            _before.uniswapV3Pool_feeGrowthGlobal0X128,
            _after.uniswapV3Pool_feeGrowthGlobal0X128,
            _before.uniswapV3Pool_feeGrowthGlobal1X128,
            _after.uniswapV3Pool_feeGrowthGlobal1X128
        );
```

我们可以通过在根目录下运行以下命令来运行上述实现此断言的测试：

`echidna test/recon/CryticTester.sol --contract CryticTester --config echidna.yaml`

**注意**：如果你使用附带的仓库，你将需要更改 Chimera 子模块依赖项，以解决不兼容的 Solidity 编译器版本，从而使 Echidna 能够运行。你需要将所有出现的 `pragma solidity ^0.8.0` 替换为 `pragma solidity ^0.7.6`，并在 `Hevm.sol` 中将 pragma 语句替换为 `pragma abicoder v2`。

从结果中我们可以看到，测试通过，意味着没有断言失败：

![](https://img.learnblockchain.cn/2025/03/08/F4669f4e9-755a-4300-b1fb-0442e7aaa11c_1008x452.png)

现在，为了确保我们的测试适当地验证了我们所希望的属性，我们可以在 [line 724](https://github.com/nican0r/recon-uniswapv3/blob/4dc51766bc56e696b5f134dfe3b08af725b61955/contracts/UniswapV3Pool.sol#L724) 的 `swap` 函数中引入一个突变，使得如果价格没有改变，则将该刻度的流动性设置为 0：

```
// shift tick if we reached the next price
            if (state.sqrtPriceX96 == step.sqrtPriceNextX96) {
                ...
            } else if (state.sqrtPriceX96 != step.sqrtPriceStartX96) {
                // recompute unless we're on a lower tick boundary (i.e. already transitioned ticks), and haven't moved
                state.tick = TickMath.getTickAtSqrtRatio(state.sqrtPriceX96);
                // 突变
                state.liquidity = 0;
            }
```

当我们再次运行 echidna 时，可以看到这是在 `test_swap_exactOut_zeroForOne` 函数中被违反了：

![](https://img.learnblockchain.cn/2025/03/08/2Fb9cf4460-b623-4f33-ae4d-5a7d3d7d2b88_740x208.png)

这表明如果价格保持不变，我们的属性测试确实捕获了系统的错误功能，这将导致刻度范围内的流动性发生变化，并让我们对测试的正确性有了更多信心。

## 加强套件

Recon 提供了一种工具来减少设置测试套件所需的时间。

在上述示例中，我们展示了如何借助这个工具复制 Uniswap V3 的现有测试套件的一部分，只需手动设置所需的一小部分。

这是 Recon 所提供的核心价值，减少实施测试套件所需的时间，使你可以专注于编写测试，而不是配置测试工具。

**我非常感谢 [Nican0r](https://twitter.com/nican0r) 创建了这本关于如何在 Uniswap v3 上使用 Recon 的深入指南。**

* * *

#### 订阅所有模糊相关内容

一年前启动

我们讨论模糊测试、不变性测试、符号测试和形式验证。

>- 原文链接： [allthingsfuzzy.substack....](https://allthingsfuzzy.substack.com/p/7f445387-8f26-426a-b3f0-d6b5a64043e1)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

Feb 24, 2024

什么是 Recon？

Recon 是一款加速编写不变性测试过程的工具。它可以连接到任何开源的 Solidity 项目，并自动生成用于创建 Echidna、Medusa 和 Foundry 的不变性测试的骨架代码，只需几次点击。

开发者和审计员可以不再花费数小时来设置测试套件，而是将精力集中在创建可能发现其系统中漏洞的相关属性上。

它是如何工作的

在本次测试工具演示中，我们将使用 Uniswap v3 仓库，因为大多数审计员和开发者都熟悉这个代码库。

在发布之前，Uniswap V3 经过了 Trail of Bits 的审计，他们扩展了现有的 Echidna 测试套件并定义了应该在整个系统中保持的属性。在这个示例中我们要关注的属性是：

如果调用 swap 不改变 sqrtPriceX96，流动性将不会改变（Property-17）

我们将看到如何在几个步骤中使用 Recon 创建一个新的测试套件，并开始测试这个属性。

下面示例创建的仓库可在这里找到。

项目设置

点击“开始工作”将启动 Recon 云服务上的构建任务，该任务将返回项目中的所有合约，并能够选择添加到测试工具中的功能。

由于在本演示中，我们只会测试与 Pool 合约函数和 TestERC20 状态变量相关的属性，因此我们不需要从目标合约中选择任何函数。如果我们要创建 Echidna 布尔属性测试以对特定函数的输入值进行模糊测试，我们将在此选择感兴趣的函数，并在 Properties 合约中定义我们的属性。在我们的使用案例中，我们保留 mint 和 swap 函数，以防将来决定从“构建处理程序”页面添加布尔属性测试，并取消选择（以红色标记）所有不感兴趣的函数：

在“前后跟踪器”标签中，我们可以选择在 Pool 合约中要跟踪的状态变量，以便进行断言，这类似于 Certora 或 Foundry 教程中的“幽灵变量”。

在我们的案例中，我们将仅使用来自 TestERC20 合约的 balanceOf 和 UniswapV3Pool 中的 feeGrowthGlobal0X128、feeGrowthGlobal1X128、liquidity、slot0 和 ticks，因为这些是我们需要证明流动性属性的全部内容：

一旦我们选择了这些变量，我们可以看到“结果页面”，在这里我们可以访问所有测试工具的文件：

TargetFunctions.sol

此文件为我们感兴趣的合约函数提供了一个入口点，Echidna/Medusa/Foundry 在运行布尔属性测试时会调用这些函数，并且是我们可以定义断言测试的地方。

BeforeAfter.sol

此文件提供了合约变量的幽灵副本，这些副本存储在一个结构中，并通过调用 __before 和 __after 函数进行更新。它们简化了访问合约中状态变量值的过程，使其更容易通过存储幽灵变量的 _before 和 _after 结构进行访问。

Setup.sol

Setup 合约简单地用于部署系统所需的所有合约。由于每个系统的部署可能是特定的，因此需要手动修复，这就是为什么默认值是对测试套件实施者的 TODO。在这个示例中，由于与 UniswapVPool 的一些奇怪之处，我们在此没有实例化它，而是使用 _init 函数。

CryticToFoundry.sol

CryticTester.sol

这是进入 Echidna 和 Medusa 的主要入口，以调用模糊测试合约。

Properties.sol

在这里，你将编写需要在感兴趣的合约上测试的属性。

medusa.json 和 echidna.yaml

这些只是用于配置 Echidna 和 Medusa 的配置文件，用于调整运行测试期间模糊测试器的设置。

运行模糊测试器

设置

Recon 默认配置 Echidna 以对函数名以 invariant_ 开头的布尔属性测试，而不是标准的 echidna_ 前缀。

我们将使用 Trail of Bits 团队为上述选择的属性创建的断言测试，并进行了修改，以便它们可以与 Recon 创建的工具正常工作。由于这些测试是断言测试，因此需要调用合约函数以验证特定状态，因此我们将它们定义在 TargetFunctions 合约中，而不是在 Properties 中，我们可以使用任何前缀来命名，因此使用 test_。

注意：附带的仓库已包含以下设置步骤，但如果你使用自己的仓库，你需要遵循这些步骤以添加 Recon 工具。

对于不使用 Foundry 的项目：由于 Uniswap V3 仓库未实现 Foundry，因此我们首先需要通过 forge install 来添加它。这使我们能够使用 Foundry 的增强调试工具来调试问题，并为在模糊测试活动过程中可能发现的任何失败案例创建 Foundry 测试。

在 Recon 的“结果页面”中，你将有机会下载从创建工具生成的文件，这些文件应添加到 Foundry 创建的 tests/ 目录中。

我们还需要通过 forge install Recon-Fuzz/chimera 来添加 Chimera 依赖项，帮助配置我们的项目以使用 Recon 工具。

然后我们在 foundry.toml 文件中将 Chimera 添加到我们的重映射中，并添加一些配置以确保 CryticCompiler 与 Uniswap 使用的 solc 编译器版本兼容：

[profile.default]
remappings = [\
    'forge-std/=lib/forge-std/src/',\
    '@chimera/=lib/chimera/src/'\
]
solc = "0.7.6"
evm_version = "istanbul"

Swap 属性测试

对于我们想要测试的属性：

如果调用 swap 不改变 sqrtPriceX96，流动性将不会改变

我们在 Setup 合约中定义了一个检查此属性的断言：

function check_swap_invariants(
        int24 tick_bfre,
        int24 tick_aftr,
        uint128 liq_bfre,
        uint128 liq_aftr,
        uint256 bal_sell_bfre,
        uint256 bal_sell_aftr,
        uint256 bal_buy_bfre,
        uint256 bal_buy_aftr,
        uint256 feegrowth_sell_bfre,
        uint256 feegrowth_sell_aftr,
        uint256 feegrowth_buy_bfre,
        uint256 feegrowth_buy_aftr
    ) internal {
        // 属性 #17
        if (tick_bfre == tick_aftr) {
            assert(liq_bfre == liq_aftr);
        }
    }

该断言将在 TargetFunctions 中的以下测试函数中进行评估：test_swap_exactIn_zeroForOne、test_swap_exactIn_oneForZero、test_swap_exactOut_zeroForOne 和 test_swap_exactOut_oneForZero。

我们的测试使用 BeforeAfter 合约提供的前后幽灵变量来检查系统的状态，并确保属性没有被违反：

        __before();
        swapper.doSwap(true, _amountSpecified, sqrtPriceLimitX96);
        __after();

        int24 beforeCurrentTick = _before.uniswapV3Pool_currentTick;
        int24 afterCurrentTick = _after.uniswapV3Pool_currentTick;

        check_swap_invariants(
            beforeCurrentTick,
            afterCurrentTick,
            _before.uniswapV3Pool_liquidity,
            _after.uniswapV3Pool_liquidity,
            _before.testERC20_balanceOfToken0,
            _after.testERC20_balanceOfToken0,
            _before.testERC20_balanceOfToken1,
            _after.testERC20_balanceOfToken1,
            _before.uniswapV3Pool_feeGrowthGlobal0X128,
            _after.uniswapV3Pool_feeGrowthGlobal0X128,
            _before.uniswapV3Pool_feeGrowthGlobal1X128,
            _after.uniswapV3Pool_feeGrowthGlobal1X128
        );

我们可以通过在根目录下运行以下命令来运行上述实现此断言的测试：

echidna test/recon/CryticTester.sol --contract CryticTester --config echidna.yaml

注意：如果你使用附带的仓库，你将需要更改 Chimera 子模块依赖项，以解决不兼容的 Solidity 编译器版本，从而使 Echidna 能够运行。你需要将所有出现的 pragma solidity ^0.8.0 替换为 pragma solidity ^0.7.6，并在 Hevm.sol 中将 pragma 语句替换为 pragma abicoder v2。