在外部审计前 使用不变性模糊测试之前找到高风险漏洞

• 原文链接：dacian.me/find-highs-b...
• 译者：AI翻译官，校对：翻译小组
• 本文链接：learnblockchain.cn/article…

在外部审计的私密审计中发现的许多高严重性问题，本来可以通过协议开发者在聘请外部审计员之前，利用不变性模糊测试(Invariant Fuzz Testing)自行发现。虽然这不需要培养“攻击者心态”或其他审计员特定技能，但确实需要学习以不变性思考，这对于协议开发者和智能合约审计员来说都是一种有用的技能。

考虑到“一级”外部审计公司收取的费用，提前在内部进行不变性测试以避免外部审计，更具成本效益。尤其是因为协议开发者对重要的协议和合约属性已具有全面了解，因此可以更快速地编写不变性。

以不变性思考

开发者需要获得的主要技能是学习以不变性思考。我之前提供了一个简单的 框架，该框架：

• 使用 Chimera 编写一个可以跨越 Echidna、Medusa 和 Foundry 模糊器工作的代码库，并允许使用 Recon 进行简单的 云模糊测试

• 将 合约生命周期 分为至少 3 个阶段：构建/初始化、常规运行和一个可选的结束状态

• 将 不变性分为两大类：可以从协议设计和文档中获得的“黑盒”不变性，以及基于智能合约内部实现代码的“白盒”不变性

不变性还可以进一步分类为以下类型：

• 相关存储位置之间的关系，例如：
  - 映射 X 中所有值的总和必须等于存储中其他地方存储的 Y（常规，白盒）
  - 所有出现在可枚举集合 X 中的地址必须也作为键存在于映射 Y 中（常规，白盒）

• 合约/协议持有的货币价值和偿付能力要求，例如：
  - 一旦代币/奖励/收益分配完成，合约应有 0 余额（结束状态，黑盒）
  - 合约应始终有足够的代币来覆盖负债（常规，黑盒）

• 防止无效状态的逻辑不变性，例如：
  - 拥有活动借款的账户不能退出其借款的市场（常规，黑盒）
  - 协议永远不应进入可以被清算但不能偿还的状态（常规，黑盒）

• 由于意外错误导致的拒绝服务（DoS），例如：
  - 清算永远不应因意外错误（如数组越界、溢出/下溢等）而回退（常规，白盒）

处理程序与无处理程序

不变性模糊测试器可以使用“处理程序”函数，这些函数包装目标合约中的底层函数，满足预备条件以防止简单回退。或者，模糊测试器也可以不使用处理程序，这允许模糊测试器自由探索。这两种选择之间的权衡为：

• 当不使用处理程序时，如果搜索空间过大，模糊测试器可能没有足够的时间找到违反不变性的序列，并且可能由于简单回退而浪费了许多运行

• 使用处理程序消除了由于简单回退而浪费的运行，提高了模糊测试效率，但也限制了搜索空间，因此可能会错过某些违反不变性的序列

一般来说，大多数开发者会希望使用处理程序，以通过满足基本预备条件来提高模糊测试的效率，同时注意不要过于限制模糊输入。

示例 1 - 闪电贷拒绝服务

规范：存在两个合约 Receiver 和 Lender。 Receiver 具有一个函数 executeFlashLoan，该函数调用 Lender::flashLoan 进行闪电贷，而重要的不变性是，如果 Lender 有足够的代币可用，Receiver 应始终能够进行闪电贷。仅根据此规范，甚至不查看代码，我们可以编写一个（常规，黑盒）不变性，如 此处：

function invariant_receiver_can_take_flash_loan() public returns (bool result) {
    receiver.executeFlashLoan(10);
    result = true;
}

通过检查 Lender::flashLoan 的 实现，我们可以基于该函数的工作原理写出一个更具体的（常规，白盒）不变性：

function invariant_pool_bal_equal_token_pool_bal() public view returns(bool result) {
    result = pool.poolBalance() == token.balanceOf(address(pool));
}

一般来说，模糊测试器更容易破坏第二个更具体的白盒不变性，较难破坏第一个更一般的黑盒不变性。在这种情况下，Foundry、Echidna 和 Medusa 都可以破坏这两个不变性。

这些不变性都不需要任何特殊的审计员特定技能来编写；协议开发者可以轻松地将这些不变性作为协议测试套件的一部分。

虽然这不是一个真实的代码库，但它来自 Damn Vulnerable DeFi 的 Unstoppable 挑战，以下所有简化示例将来自我在与 Cyfrin 合作时对真实代码库的私密审计结果。

示例 2 - 奖励分配卡住

规范：一个由 DAO 部署的 Proposal 合约，分配一些 ETH，如果提案成功：

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

• 在活动期间，合格的投票者可以投票 支持 或 反对

• 如果达到法定人数，ETH 应在 支持 投票者之间分配

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

在不查看实现的情况下，我们可以写出一个黑盒 不变性，该不变性涵盖了常规运行和结束状态：

    function property_proposal_complete_all_rewards_distributed() public returns(bool) {
        uint256 proposalBalance = address(prop).balance;

        // 仅在不变性失败时可见
        emit ProposalBalance(proposalBalance);

        return(
            // 方案要么是活动的并且合约余额 > 0
            (prop.isActive() && proposalBalance > 0) ||

            // 或者方案不是活动的并且合约余额 == 0
            (!prop.isActive() && proposalBalance == 0)
        );
    }

这个不变式揭示了一个高严重性问题，导致代币永久卡在合约中。

示例 3 - 投票权力破坏

规范：一个 VotingNft 合约：

• 允许用户存入 ETH 抵押品以获得其 NFT 的 DAO 投票权

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

• 一旦权力计算开始，所有 NFT 从最大投票权开始，未被存入 ETH 支持的 NFT 的投票权会随时间下降

• 投票权下降的 NFT 的投票权永远无法增加；存入所需的 ETH 抵押品仅能防止未来的任何下降

仅从这个规范中，我们可以编写一个（初始化，黑盒） 不变式来验证当权力计算开始时，所有 NFT 的总投票权等于最大投票权乘以创建的 NFT 数量：

    function property_total_power_eq_init_max_power_calc_start() public view returns(bool result) {
        result = votingNft.getTotalPower() == initMaxNftPower;
    }

这个非常简单的不变式揭示了两个严重问题：

• 一个严重的不对称漏洞，允许无权限攻击者利用该漏洞将每个 NFT 的投票权永久设置为 0

• 一个高漏洞，允许无权限攻击者在保持单个 NFT 投票权的同时，显著降低总投票权至接近 0，从而大幅增加任何 NFT 持有者的投票权

示例 4 - 代币销售耗尽

规范：一个 TokenSale 合约：

• 允许 DAO 将其治理 sellToken 以换取另一个 buyToken

• 代币销售仅针对允许的用户，每个用户最多只能购买到最大限额，以防止投票权集中

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

仅使用规范，我们可以创建两个（常规，黑盒）不变式。第一个不变式( 第一不变式 )验证购买的代币数量与出售的代币数量相匹配（由于简化的 1:1 交换）：

    function invariant_tokens_bought_eq_tokens_sold() public view returns(bool result) {
        uint256 soldAmount = tokenSale.getSellTokenSoldAmount();
        uint256 boughtBal  = buyToken.balanceOf(address(this));

        // 根据精度差异放大 `boughtBal`
        // SELL_DECIMALS >= BUY_DECIMALS
        boughtBal *= 10 ** (SELL_DECIMALS - BUY_DECIMALS);

        result = (boughtBal == soldAmount);
    }

第二个不变式( 第二不变式 )验证用户只能购买到每个用户允许的最大 sellToken 数量：

    function invariant_max_token_buy_per_user() public view returns(bool result) {
        for(uint256 i; i<buyers.length; ++i) {
            address buyer = buyers[i];

            if(sellToken.balanceOf(buyer) > MAX_TOKENS_PER_BUYER) {
                return false;
            }
        }

        result = true;
    }

这两个简单的不变式揭示了：

• 一个严重的向下舍入到零漏洞，由我的队友发现，允许用户获得免费代币

• 一个高漏洞，允许用户绕过每个用户的最大购买代币限制，购买所有代币，从而获得主导投票权

示例 5 - 归属积分增加

规范：一个 Vesting 合约为用户分配积分，这些积分可以在其归属期结束后用于兑换代币。该合约在constructor中实现了一个初始化不变式 ，确保所有积分都已分配：

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

用户可以将其积分转移到另一个地址，但除此之外，用户没有办法增加或减少其分配的积分，因此所有用户积分的总和应始终等于初始分配的总和。

根据规范，我们可以编写一个（常规，黑盒） 不变式来验证所有用户积分的总和始终等于初始分配的总积分：

    function property_users_points_sum_eq_total_points() public view returns(bool result) {
        uint24 totalPoints;

        // 使用 `recipients` 幽灵变量汇总所有用户积分
        for(uint256 i; i<recipients.length; i++) {
            (uint24 points, , ) = vesting.allocations(recipients[i]);

            totalPoints += points;
        }

        // 如果不变式成立则为真，否则为假
        if(totalPoints == TOTAL_POINTS) result = true;

        // 注意：Solidity 总是初始化为默认值
        // 所以不需要显式设置 result = false，因为 false
        // 是 bool 的默认值
    }

这个不变式暴露了一个高严重性漏洞，允许用户给自己无限数量的积分，从而耗尽代币分配。

示例 6 - 提前认领滥用

规范：一个 VestingExt 合约具有与之前的 Vesting 合约相同的功能，另外还增加了一项功能，让用户可以 preclaim 部分代币配额，使用户在满足其归属期之前获得有限数量的代币。

仅使用规范，我们可以创建一个（常规，黑盒） 不变式 ，它验证总的提前认领点数始终小于或等于最大可认领点数（这就是用户数量乘以每个用户的最大提前认领点数）：

function property_total_preclaimed_lt_eq_max_preclaimable() public view returns(bool result) {
    result = totalPreclaimed <= MAX_PRECLAIMABLE;
}

这个不变式发现了一个 中等 严重性漏洞，允许用户提前认领其全部代币配额，而在审计代码的情况下，迅速获得超出其应有的 DAO 投票权。

示例 7 - 操作员注册表腐败

规范：一个 OperatorRegistry 合约允许用户注册为操作员并接收一个 operatorId，其中第一个 operatorId = 1，后续的 ID 递增。

合约存储有多个相互关联的数据结构，使用用户的 address 和 operatorId 作为映射中的键来相互引用，从而能够通过 address 或 operatorId 查询操作员数据。用户还可以更新他们的 address。

从这个规范中，我们可以编写一个（常规，黑盒） 不变式 ，它通过确保每个 operatorId 与唯一的 address 相关来验证这些相互关联的数据结构的数据完整性：

EnumerableSet.AddressSet foundAddresses;

function property_operator_ids_have_unique_addresses() public returns(bool result) {
    // 首先从幽灵存储中移除旧的找到的
    uint256 oldFoundLength = foundAddresses.length();
    if(oldFoundLength > 0) {
        address[] memory values = foundAddresses.values();

        for(uint256 i; i<oldFoundLength; i++) {
            foundAddresses.remove(values[i]);
        }
    }

    // 然后遍历每个当前操作员，获取其地址
    // 并尝试将其添加到找到的集合中。如果添加失败，则为
    // 重复项，违反不变式
    uint128 numOperators = operatorRegistry.numOperators();
    if(numOperators > 0) {
        // 操作员 ID 从 1 开始
        for(uint128 operatorId = 1; operatorId <= numOperators; operatorId++) {
            if(!foundAddresses.add(operatorRegistry.operatorIdToAddress(operatorId))) {
                return false;
            }
        }
    }

    result = true;
}

这个不变式揭示了一个 低 严重性问题，我的队友发现两个不同的 operatorIds 可以指向同一个用户 address 和相关数据，破坏相互关联的数据结构关系。这在我们的审计中是一个低严重性问题，因为触发腐败的函数是受权限控制的，影响有限，但根据腐败如何被触发和利用，这在其他代码库中可能很容易成为中等或高严重性问题。

示例 8 - 强制清算拒绝服务

规范：一个 LiquidateDos 合约允许交易者进入多个市场并在每个市场中有一个开放头寸。交易者也可以被强制清算：

• 在确定交易者是否可被清算时，所有开放头寸都会被计算

• 如果被清算，则被清算的交易者的所有开放头寸都会关闭

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

使用这个规范，我们可以编写一个（常规，白盒）不变式，验证 liquidate 函数不会因意外错误而回滚。这个不变式是白盒的，因为它要求我们知道 liquidate 的具体实现细节，以便知道哪些错误是预期的。

在实施 DoS 不变式模糊测试时，有两种方法：

1. 在 assertion 模式下运行 Echidna 和 Medusa，并在模糊处理程序中有断言，但这在 Foundry 中无法工作

2. 有一个 bool 幽灵变量，在模糊处理程序中设置，然后将不变式包装在它周围 - 这适用于所有 3 个模糊器

以下是使用第二种实现的 处理程序 和 不变式：

// TargetFunctions 模糊处理程序
function handler_liquidate(uint8 victimIndex) external {
    address victim = _getRandomAddress(victimIndex);

    try liquidateDos.liquidate(victim) {
        // 更新幽灵变量
        delete userActiveMarketsCount[victim];

        for(uint8 marketId = liquidateDos.MIN_MARKET_ID();
            marketId <= liquidateDos.MAX_MARKET_ID();
            marketId++) {
            delete userActiveMarkets[victim][marketId];
        }
    }
    catch(bytes memory err) {
        bytes4[] memory allowedErrors = new bytes4[](2);
        allowedErrors[0] = ILiquidateDos.LiquidationsDisabled.selector;
        allowedErrors[1] = ILiquidateDos.LiquidateUserNotInAnyMarkets.selector;

        if(_isUnexpectedError(bytes4(err), allowedErrors)) {
            liquidateUnexpectedError = true;
        }
    }
}

// 返回错误是否意外
function _isUnexpectedError(
    bytes4 errorSelector,
    bytes4[] memory allowedErrors
) internal pure returns(bool isUnexpectedError) {
    for (uint256 i; i < allowedErrors.length; i++) {
        if (errorSelector == allowedErrors[i]) {
            return false;
        }
    }

    isUnexpectedError = true;
}

// 属性不变式
function property_liquidate_no_unexpected_error() public view returns(bool result) {
    result = !liquidateUnexpectedError;
}

这个不变式发现了一个 严重 严重性漏洞，交易者可以利用这个漏洞使自己无法被清算。

示例 9 - 稳定池排水

规范：一个 StabilityPool 合约，它：

• 允许用户存入 debtToken，用于在清算过程中偿还坏账

• 作为交换，debtToken 存款人从清算过程中扣押的抵押物中获得一部分 collateralToken 奖励

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

• 必须始终保持偿付能力；池中应始终有足够的 collateralToken 来支付应付给 debtToken 存款人的奖励

一个自然从规范中流出的 (常规的黑盒) 不变式 是验证池的偿付能力：

function property_stability_pool_solvent() public view returns(bool result) {
    uint256 totalClaimableRewards;

    // 计算每个用户的可领取奖励总额
    for(uint8 i; i<ADDRESS_POOL_LENGTH; i++) {
        address user = addressPool[i];

        totalClaimableRewards += stabilityPool.getDepositorCollateralGain(user);
    }

    // 如果可领取的奖励总额小于等于抵押代币余额，则池是偿付的
    if(totalClaimableRewards <= collateralToken.balanceOf(address(stabilityPool)))
        result = true;
}

这个简单的不变式揭示了一种 致命 漏洞，该漏洞出现在我审计的代码所分叉出来的原始协议中。这个漏洞是通过一个 “小修复” 引入的，并在代码库中潜伏了 1 年；它允许一个 debtToken 存款人完全抽走 StabilityPool 中的所有 collateralTokens。

这个不变式的简单性展示了不变式模糊测试的巨大威力：在不了解复杂的奖励计算代码的情况下，我们可以编写一个简单的黑盒不变式，而模糊测试工具会通过找到一个极其有价值的致命漏洞来破坏它。

示例 10 - 抵押优先级腐败

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

• 定义抵押物的清算优先级顺序

• 当发生清算时，风险最高的抵押物会优先清算，以便借款人在清算后剩余的抵押物更加稳定

• 允许添加和移除抵押物；添加时总是将新抵押物放在优先队列的末尾，而移除时则保留现有顺序，去掉被移除的元素

从规范中，我们可以编写一个 (常规的黑盒) 不变式 来验证抵押物的顺序始终正确。为了简化我们在模糊测试中的实现，我们使用 4 个抵押物，更新模糊 处理函数 中的预期顺序，然后将预期顺序与不变式中的实际顺序进行比较：

// 目标函数模糊处理器更新幽灵变量预期顺序
function handler_addCollateral(uint8 collateralId) external {
    collateralId = uint8(between(collateralId,
                                 priority.MIN_COLLATERAL_ID(),
                                 priority.MAX_COLLATERAL_ID()));

    priority.addCollateral(collateralId);

    // 更新幽灵变量以反映预期顺序
    if(priority0 == 0) priority0 = collateralId;
    else if(priority1 == 0) priority1 = collateralId;
    else if(priority2 == 0) priority2 = collateralId;
    else priority3 = collateralId;
}

function handler_removeCollateral(uint8 collateralId) external {
    collateralId = uint8(between(collateralId,
                                 priority.MIN_COLLATERAL_ID(),
                                 priority.MAX_COLLATERAL_ID()));

    priority.removeCollateral(collateralId);

    // 更新幽灵变量以反映预期顺序
    if(priority0 == collateralId) {
        priority0 = priority1;
        priority1 = priority2;
        priority2 = priority3;
    }
    else if(priority1 == collateralId) {
        priority1 = priority2;
        priority2 = priority3;
    }
    else if(priority2 == collateralId) {
        priority2 = priority3;
    }

    delete priority3;
}

// 属性不变式
function property_priority_order_correct() public view returns(bool result) {
    if(priority0 != 0) {
        if(priority.getCollateralAtPriority(0) != priority0) return false;
    }
    if(priority1 != 0) {
        if(priority.getCollateralAtPriority(1) != priority1) return false;
    }
    if(priority2 != 0) {
        if(priority.getCollateralAtPriority(2) != priority2) return false;
    }
    if(priority3 != 0) {
        if(priority.getCollateralAtPriority(3) != priority3) return false;
    }

    result = true;
}

这个不变式揭示了一种 高 漏洞，该漏洞破坏了抵押优先级顺序，导致错误的抵押物被优先清算，结果造成交易者在清算后留下了更不健康的抵押物，从而增加了未来清算的可能性。

结论

我们回顾了我在真实代码库进行的 9 个简化示例，其中不变式模糊测试本可以被协议开发者“内部”使用，以检测和修复重要漏洞，从而在与外部审计人员合作之前。

这 9 个不变式中只有 1 个是白盒，这意味着编写它需要理解智能合约的内部实现细节。其他 8 个都是黑盒，可以简单地从协议或合约规范中推导出来。所有 9 个不变式相对都是简单易写和实现的。

协议开发者和智能合约审计员可以通过学习以不变式思维，且将不变式模糊测试作为他们工作的一部分，显著提高其协议的安全性。

我是 AI 翻译官，为大家转译优秀英文文章，如有翻译不通的地方，在这里修改，还请包涵～