模糊/不变式测试 – ImmuneBytes

文章介绍了模糊测试和不变式测试在智能合约安全中的重要性,旨在发现传统单元测试可能遗漏的边缘漏洞。它解释了不变式作为协议核心属性的重要性,并探讨了无状态、有状态模糊测试、有界模型检测以及结合端到端测试等多种方法,以全面提升智能合约的安全性。

三月 2, 2026

引言

让我们首先了解攻击是如何发生的。在大多数情况下,软件中的安全漏洞是你在单元测试期间没有预料到的边缘情况造成的,因此也没有为其编写测试。但是,如果我告诉你有一种方法,可以通过单一的方法来解决这些不可预测的情况,这种方法可以对几乎所有可能性进行压力测试,那会怎么样?

什么是模糊测试,以及如何将其应用于 Solidity 智能合约?

我们将从理解模糊测试本身开始,到本文结束时,将其与 Solidity 智能合约联系起来。现在,如果你是为了模糊测试的正式教科书定义而来,我会为你省去麻烦,因为那不是你想要的,对吗?🙂

让我为你简化一下。在编写测试时,目标通常是达到 100% 的代码覆盖率。然而,即使有了完美的覆盖率,你也不能保证代码中没有潜藏的错误。这就是模糊器发挥作用的地方。模糊器生成一系列输入,用于测试你在单元测试中可能遗漏的边界

正式定义为:“模糊测试(或 fuzzing)涉及向系统模拟器馈送随机数据,以试图破坏它。”

然而,模糊测试的有效性取决于你编写的模糊测试的质量。模糊器作为软件工具,本质上是不智能的。它们在计算边界内运行,缺乏上下文或决策能力。

例如,在一个具有多种可能操作的系统中,模糊器可能会随机选择一个不恰当的操作。以 onlyOwner 函数为例——如果模糊器使用一个无效地址,它自然会触发一次回滚。这类情况是可预测且微不足道的,通常被归类为低垂的果实。由于你预期到这些故障,它们应该已经在单元测试中被覆盖。

为了避免将宝贵的模糊测试资源浪费在这些不相关的场景上,绕过明显的故障并专注于重要的边缘情况至关重要。因此,编写有效的模糊测试,就是要从该过程中榨取最大的价值。

引入不变量:必须始终保持的核心属性

现在我们来谈谈不变量,也称为属性。这部分会稍微细致一些,但并没有看起来那么复杂。简单来说,不变量是你断言必须始终保持为真的属性或规则。

与单元测试不同,单元测试中你提供单个输入并验证预期结果,而不变量测试则验证某个特定属性在许多随机输入下都成立。模糊器会使用各种值反复测试这些属性,确保系统在所有场景下都按预期运行。

让我进一步简化。在 DeFi 的世界中,不变量是协议赖以维持稳定性和公平性的基本规则。这些是无论执行何种操作,都绝不能被打破的“法律”。

借贷市场不变量

在 Compound 或 Aave 等借贷协议中,一个关键规则是用户的借款价值绝不能超过其抵押品。进一步解释,当你借款时,你必须存入价值高于借款价值的抵押品。这类似于抵押贷款,你不能借款超过你房屋的价值。协议会阻止任何会将账户置于不安全状态或恶化已风险状况的操作。

AMM 不变量

自动做市商(Automated Market Makers),如 Uniswap 或 SushiSwap,依赖于一个数学不变量来维持流动性池的平衡。该规则表示为 $x * y = k$,其中 $x$ 和 $y$ 代表代币数量,而 $k$ 是一个常量。如果有人购买更多的一种代币,价格会按比例上涨以保持不变量。

质押/流动性挖矿不变量

质押协议中,有一个简单但至关重要的规则:用户只能提取他们最初存入的相同数量的代币。例如,如果你质押 10 个代币,你就可以精确地提取回 10 个代币。虽然通过质押可以获得奖励,但本金金额保持不变。

示例时间?

pragma solidity ^0.8.0;
contract UniswapInvariantCheck {
    uint256 public reserveX; // 代币 X 的储备
    uint256 public reserveY; // 代币 Y 的储备

    constructor(uint256 _initialX, uint256 _initialY) {
        reserveX = _initialX; // 初始化储备
        reserveY = _initialY; // 初始化储备
    }

    // 模拟代币互换的函数
    function swap(uint256 inputX, uint256 inputY) public {
        require(inputX == 0 || inputY == 0, "Only one token can be swapped"); // 确保只互换一种代币
        if (inputX > 0) {
            // 代币 X 被互换入池
            uint256 newReserveX = reserveX + inputX; // 更新 X 的储备
            uint256 newReserveY = (reserveX * reserveY) / newReserveX; // 使用不变量计算 Y 的新储备
            reserveX = newReserveX; // 更新状态
            reserveY = newReserveY; // 更新状态
        } else if (inputY > 0) {
            // 代币 Y 被互换入池
            uint256 newReserveY = reserveY + inputY; // 更新 Y 的储备
            uint256 newReserveX = (reserveX * reserveY) / newReserveY; // 使用不变量计算 X 的新储备
            reserveX = newReserveX; // 更新状态
            reserveY = newReserveY; // 更新状态
        }
    }

    // 检查不变量是否保持的函数
    function invariantHolds() public view returns (bool) {
        uint256 k = reserveX * reserveY; // 计算常数 k
        return k == reserveX * reserveY; // 验证 x * y = k 是否成立
    }
}
  1. 不变量规则 ($x * y = k$):
  • 在 Uniswap V3 中,reserveXreserveY 代表流动性池中两种代币的数量。
  • 不变量 $x * y = k$ 确保这些储备的乘积在互换过程中保持不变。这条规则是维持代币价格平衡的基础。
  1. 互换函数如何工作:
  • 输入验证swap 函数确保一次只互换一种代币($X$ 或 $Y$)(require(inputX == 0 || inputY == 0))。
  • 更新储备:如果互换代币 $X$,则使用不变量公式计算 $Y$ 的新储备:

newReserveY = (reserveX * reserveY) / newReserveX

  • 同样,如果互换代币 $Y$,则计算 $X$ 的新储备:

newReserveX = (reserveX * reserveY) / newReserveY

  • 不变量验证

invariantHolds 函数检查 reserveXreserveY 的乘积是否保持一致。如果任何操作破坏了这种平衡,不变量将不成立,表明实现或逻辑中存在问题。

无状态与有状态模糊测试:两种破坏系统的方法

为了理解模糊测试技术,让我们用易碎玻璃的类比。

无状态模糊测试独立测试每个场景。想象一下测试一个玻璃杯,通过:

  1. 用勺子敲击它。
  2. 往里面扔一块小石子。
  3. 把它摔到地上。

在每种情况下,你都使用一个全新的玻璃杯。过去的操作不会影响下一次测试。虽然这种方法速度快,但它忽略了早期操作可能如何影响结果。

另一方面,有状态模糊测试在所有测试中都使用同一个玻璃杯。如果你在第一步敲击玻璃杯,第二步往里扔一块小石子,第三步把它摔出去,你就会观察到累积效应。这种方法反映了真实世界中的系统,其中先前的操作会影响未来的行为,从而揭示更深层次的错误。

有限模型检查(BMC):为有效测试设置限制

有限模型检查(BMC)通过限制识别错误的步骤来改进模糊测试。BMC 没有无休止地探索输入,而是设置了逻辑上的“界限”。

例如,向 AMM 存入零代币可能会触发 MIN_INITIAL_SHARES 错误。由于这是一个可预测的故障,你可以引导模糊器避免此类输入,转而关注有意义的边缘情况

将 BMC 视为导航迷宫。你决定只检查少于 10 步的路径。如果错误存在于这些界限内,你就会找到它。否则,系统在该范围内保持稳定。

端到端测试与模糊测试的结合:完美的组合

端到端(E2E)测试模拟真实世界用户的操作,确保系统按预期运行。例如,注册表单的 E2E 测试将验证各种输入:空白字段、无效电子邮件和有效凭据。

当与模糊测试结合时,E2E 测试变得更加强大。E2E 测试检查正常工作流程,而模糊测试引入不可预测性,以测试系统在压力下的响应。它们共同提供了一个强大的框架,用于验证预期和意外行为。

结论:

模糊测试是发现传统测试可能遗漏的隐藏漏洞的颠覆性技术。通过将模糊测试与不变量测试相结合,我们超越了仅仅测试单个函数,而是关注系统的整体行为和稳定性。有状态模糊测试有限模型检查端到端测试等方法协同工作,以揭示边缘情况并使智能合约更加安全。

  • 原文链接: blog.immunebytes.com/fuz...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
ImmuneBytes
ImmuneBytes
Stay Ahead of the Security Curve.