{"content":{"title":"在外部审计前 使用不变性模糊测试之前找到高风险漏洞","body":">- 原文链接：[dacian.me/find-highs-b...](https://dacian.me/find-highs-before-external-auditors-using-invariant-fuzz-testing)\r\n>- 译者：[AI翻译官](https://learnblockchain.cn/people/19584)，校对：[翻译小组](https://learnblockchain.cn/people/412)\r\n>- 本文链接：[learnblockchain.cn/article…](https://learnblockchain.cn/article/10147)\r\n    \r\n在外部审计的私密审计中发现的许多高严重性问题，本来可以通过协议开发者在聘请外部审计员之前，利用不变性模糊测试(Invariant Fuzz Testing)自行发现。虽然这不需要培养“攻击者心态”或其他审计员特定技能，但确实需要学习以不变性思考，这对于协议开发者和智能合约审计员来说都是一种有用的技能。\r\n\r\n考虑到“一级”外部审计公司收取的费用，提前在内部进行不变性测试以避免外部审计，更具成本效益。尤其是因为协议开发者对重要的协议和合约属性已具有全面了解，因此可以更快速地编写不变性。\r\n\r\n## 以不变性思考\r\n\r\n开发者需要获得的主要技能是学习以不变性思考。我之前提供了一个简单的 [框架](https://dacian.me/writing-multi-fuzzer-invariant-tests-using-chimera#heading-thinking-in-invariants)，该框架：\r\n\r\n*   使用 [Chimera](https://github.com/Recon-Fuzz/chimera) 编写一个可以跨越 Echidna、Medusa 和 Foundry 模糊器工作的代码库，并允许使用 Recon 进行简单的 [云模糊测试](https://getrecon.xyz/)\r\n    \r\n*   将 [合约生命周期](https://dacian.me/writing-multi-fuzzer-invariant-tests-using-chimera#heading-contract-lifecycle) 分为至少 3 个阶段：构建/初始化、常规运行和一个可选的结束状态\r\n    \r\n*   将 [不变性分为两大类](https://dacian.me/writing-multi-fuzzer-invariant-tests-using-chimera#heading-whiteblack-box)：可以从协议设计和文档中获得的“黑盒”不变性，以及基于智能合约内部实现代码的“白盒”不变性\r\n    \r\n\r\n不变性还可以进一步分类为以下类型：\r\n\r\n*   相关存储位置之间的关系，例如：  \r\n    \\- 映射 X 中所有值的总和必须等于存储中其他地方存储的 Y（常规，白盒）  \r\n    \\- 所有出现在可枚举集合 X 中的地址必须也作为键存在于映射 Y 中（常规，白盒）\r\n    \r\n*   合约/协议持有的货币价值和偿付能力要求，例如：  \r\n    \\- 一旦代币/奖励/收益分配完成，合约应有 0 余额（结束状态，黑盒）  \r\n    \\- 合约应始终有足够的代币来覆盖负债（常规，黑盒）\r\n    \r\n*   防止无效状态的逻辑不变性，例如：  \r\n    \\- 拥有活动借款的账户不能退出其借款的市场（常规，黑盒）  \r\n    \\- 协议永远不应进入可以被清算但不能偿还的状态（常规，黑盒）\r\n    \r\n*   由于意外错误导致的拒绝服务（DoS），例如：  \r\n    \\- 清算永远不应因意外错误（如数组越界、溢出/下溢等）而回退（常规，白盒）\r\n    \r\n\r\n##  处理程序与无处理程序\r\n\r\n不变性模糊测试器可以使用“处理程序”函数，这些函数包装目标合约中的底层函数，满足预备条件以防止简单回退。或者，模糊测试器也可以不使用处理程序，这允许模糊测试器自由探索。这两种选择之间的权衡为：\r\n\r\n*   当不使用处理程序时，如果搜索空间过大，模糊测试器可能没有足够的时间找到违反不变性的序列，并且可能由于简单回退而浪费了许多运行\r\n    \r\n*   使用处理程序消除了由于简单回退而浪费的运行，提高了模糊测试效率，但也限制了搜索空间，因此可能会错过某些违反不变性的序列\r\n    \r\n\r\n一般来说，大多数开发者会希望使用处理程序，以通过满足基本预备条件来提高模糊测试的效率，同时注意不要过于限制模糊输入。\r\n\r\n##  示例 1 - 闪电贷拒绝服务\r\n\r\n规范：存在两个合约 [`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` 有足够的代币可用，`Receiver` 应始终能够进行闪电贷。仅根据此规范，甚至不查看代码，我们可以编写一个（常规，黑盒）不变性，如 [此处](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/02-unstoppable/UnstoppableBasicEchidna.t.sol#L53-L56)：\r\n\r\n    function invariant_receiver_can_take_flash_loan() public returns (bool result) {\r\n        receiver.executeFlashLoan(10);\r\n        result = true;\r\n    }\r\n    \r\n\r\n通过检查 `Lender::flashLoan` 的 [实现](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/02-unstoppable/UnstoppableLender.sol#L33-L48)，我们可以基于该函数的工作原理写出一个更具体的（常规，白盒）不变性：\r\n\r\n    function invariant_pool_bal_equal_token_pool_bal() public view returns(bool result) {\r\n        result = pool.poolBalance() == token.balanceOf(address(pool));\r\n    }\r\n    \r\n\r\n一般来说，模糊测试器更容易破坏第二个更具体的白盒不变性，较难破坏第一个更一般的黑盒不变性。在这种情况下，Foundry、Echidna 和 Medusa [都可以破坏这两个不变性](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/README.md#challenge-2-unstoppable-winner-tied-all)。\r\n\r\n这些不变性都不需要任何特殊的审计员特定技能来编写；协议开发者可以轻松地将这些不变性作为协议测试套件的一部分。\r\n\r\n虽然这不是一个真实的代码库，但它来自 [Damn Vulnerable DeFi](https://www.damnvulnerabledefi.xyz/) 的 `Unstoppable` 挑战，以下所有简化示例将来自我在与 [Cyfrin](https://www.cyfrin.io/) 合作时对真实代码库的私密审计结果。\r\n\r\n## 示例 2 - 奖励分配卡住\r\n\r\n规范：一个由 DAO 部署的 [`Proposal`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/03-proposal/Proposal.sol) 合约，分配一些 ETH，如果提案成功：\r\n\r\n*   `Proposal` 在投票结束或提案超时之前处于活动状态\r\n    \r\n*   在活动期间，合格的投票者可以投票 `支持` 或 `反对`\r\n    \r\n*   如果达到法定人数，ETH 应在 `支持` 投票者之间分配\r\n    \r\n*   否则，ETH 应退还给提案创建者\r\n    \r\n\r\n在不查看实现的情况下，我们可以写出一个黑盒 [不变性](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/03-proposal/Properties.sol#L16-L29)，该不变性涵盖了常规运行和结束状态：\r\n\r\n```javascript\r\n    function property_proposal_complete_all_rewards_distributed() public returns(bool) {\r\n        uint256 proposalBalance = address(prop).balance;\r\n    \r\n        // 仅在不变性失败时可见\r\n        emit ProposalBalance(proposalBalance);\r\n\r\n\r\n        return(\r\n            // 方案要么是活动的并且合约余额 > 0\r\n            (prop.isActive() && proposalBalance > 0) ||\r\n\r\n            // 或者方案不是活动的并且合约余额 == 0\r\n            (!prop.isActive() && proposalBalance == 0)\r\n        );\r\n    }\r\n``` \r\n\r\n这个不变式揭示了一个[高](https://solodit.xyz/issues/distributionproposal-for-voter-rewards-diluted-by-against-voters-and-missing-rewards-permanently-stuck-in-distributionproposal-contract-cyfrin-none-cyfrin-dexe-markdown)严重性问题，导致代币永久卡在合约中。\r\n\r\n##  示例 3 - 投票权力破坏\r\n\r\n规范：一个 [`VotingNft`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/04-voting-nft/VotingNftForFuzz.sol) 合约：\r\n\r\n*   允许用户存入 ETH 抵押品以获得其 NFT 的 DAO 投票权\r\n    \r\n*   NFT 可以由所有者创建，直到“权力计算开始时间”\r\n    \r\n*   一旦权力计算开始，所有 NFT 从最大投票权开始，未被存入 ETH 支持的 NFT 的投票权会随时间下降\r\n    \r\n*   投票权下降的 NFT 的投票权永远无法增加；存入所需的 ETH 抵押品仅能防止未来的任何下降\r\n    \r\n\r\n仅从这个规范中，我们可以编写一个（初始化，黑盒） [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/04-voting-nft/Properties.sol#L23-L25)来验证当权力计算开始时，所有 NFT 的总投票权等于最大投票权乘以创建的 NFT 数量：\r\n\r\n```javascript\r\n    function property_total_power_eq_init_max_power_calc_start() public view returns(bool result) {\r\n        result = votingNft.getTotalPower() == initMaxNftPower;\r\n    }\r\n```    \r\n\r\n这个非常简单的不变式揭示了两个严重问题：\r\n\r\n*   一个[严重](https://solodit.xyz/issues/attacker-can-destroy-user-voting-power-by-setting-erc721powertotalpower-and-all-existing-nfts-currentpower-to-0-cyfrin-none-cyfrin-dexe-markdown)的不对称漏洞，允许无权限攻击者利用该漏洞将每个 NFT 的投票权永久设置为 0\r\n    \r\n*   一个[高](https://solodit.xyz/issues/attacker-can-at-anytime-dramatically-lower-erc721powertotalpower-close-to-0-cyfrin-none-cyfrin-dexe-markdown)漏洞，允许无权限攻击者在保持单个 NFT 投票权的同时，显著降低总投票权至接近 0，从而大幅增加任何 NFT 持有者的投票权\r\n    \r\n\r\n## 示例 4 - 代币销售耗尽\r\n\r\n规范：一个 [`TokenSale`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/05-token-sale/TokenSale.sol) 合约：\r\n\r\n*   允许 DAO 将其治理 `sellToken` 以换取另一个 `buyToken`\r\n    \r\n*   代币销售仅针对允许的用户，每个用户最多只能购买到最大限额，以防止投票权集中\r\n    \r\n*   在我们的简化版本中，我们假设汇率为 1:1，并且 `sellToken` 的小数位数始终大于或等于 `buyToken`\r\n    \r\n\r\n仅使用规范，我们可以创建两个（常规，黑盒）不变式。第一个不变式( [第一不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/05-token-sale/TokenSaleBasicEchidna.t.sol#L124-L137) )验证购买的代币数量与出售的代币数量相匹配（由于简化的 1:1 交换）：\r\n\r\n```javascript\r\n    function invariant_tokens_bought_eq_tokens_sold() public view returns(bool result) {\r\n        uint256 soldAmount = tokenSale.getSellTokenSoldAmount();\r\n        uint256 boughtBal  = buyToken.balanceOf(address(this));\r\n    \r\n        // 根据精度差异放大 `boughtBal`\r\n        // SELL_DECIMALS >= BUY_DECIMALS\r\n        boughtBal *= 10 ** (SELL_DECIMALS - BUY_DECIMALS);\r\n    \r\n        result = (boughtBal == soldAmount);\r\n    }\r\n```\r\n\r\n第二个不变式( [第二不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/05-token-sale/TokenSaleBasicEchidna.t.sol#L143-L153) )验证用户只能购买到每个用户允许的最大 `sellToken` 数量：\r\n\r\n```javascript\r\n    function invariant_max_token_buy_per_user() public view returns(bool result) {\r\n        for(uint256 i; i<buyers.length; ++i) {\r\n            address buyer = buyers[i];\r\n    \r\n            if(sellToken.balanceOf(buyer) > MAX_TOKENS_PER_BUYER) {\r\n                return false;\r\n            }\r\n        }\r\n    \r\n        result = true;\r\n    }\r\n```\r\n\r\n这两个简单的不变式揭示了：\r\n\r\n*   一个[严重](https://solodit.xyz/issues/tokensaleproposalbuy-implicitly-assumes-that-buy-token-has-18-decimals-resulting-in-a-potential-total-loss-scenario-for-dao-pool-cyfrin-none-cyfrin-dexe-markdown)的[向下舍入到零](https://dacian.me/precision-loss-errors#heading-rounding-down-to-zero)漏洞，由我的队友发现，允许用户获得免费代币\r\n    \r\n*   一个[高](https://solodit.xyz/issues/attacker-can-bypass-token-sale-maxallocationperuser-restriction-to-buy-out-the-entire-tier-cyfrin-none-cyfrin-dexe-markdown)漏洞，允许用户绕过每个用户的最大购买代币限制，购买所有代币，从而获得主导投票权\r\n    \r\n\r\n##  示例 5 - 归属积分增加\r\n\r\n规范：一个 [`Vesting`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/09-vesting/Vesting.sol) 合约为用户分配积分，这些积分可以在其归属期结束后用于兑换代币。该合约在`constructor`中实现了一个[初始化不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/09-vesting/Vesting.sol#L37) ，确保所有积分都已分配：\r\n\r\n    require(totalPoints == TOTAL_POINTS, \"Not enough points\");\r\n    \r\n\r\n用户可以将其积分转移到另一个地址，但除此之外，用户没有办法增加或减少其分配的积分，因此所有用户积分的总和应始终等于初始分配的总和。\r\n\r\n根据规范，我们可以编写一个（常规，黑盒） [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/09-vesting/Properties.sol#L9-L25)来验证所有用户积分的总和始终等于初始分配的总积分：\r\n\r\n```javascript\r\n    function property_users_points_sum_eq_total_points() public view returns(bool result) {\r\n        uint24 totalPoints;\r\n    \r\n        // 使用 `recipients` 幽灵变量汇总所有用户积分\r\n        for(uint256 i; i<recipients.length; i++) {\r\n            (uint24 points, , ) = vesting.allocations(recipients[i]);\r\n    \r\n            totalPoints += points;\r\n        }\r\n    \r\n        // 如果不变式成立则为真，否则为假\r\n        if(totalPoints == TOTAL_POINTS) result = true;\r\n    \r\n        // 注意：Solidity 总是初始化为默认值\r\n        // 所以不需要显式设置 result = false，因为 false\r\n        // 是 bool 的默认值\r\n    }\r\n```    \r\n\r\n这个不变式暴露了一个[高](https://solodit.xyz/issues/allocationvesting-contract-can-be-exploited-for-infinite-points-via-self-transfer-cyfrin-none-bima-markdown)严重性漏洞，允许用户给自己无限数量的积分，从而耗尽代币分配。\r\n\r\n##  示例 6 - 提前认领滥用\r\n\r\n规范：一个 [`VestingExt`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/10-vesting-ext/VestingExt.sol) 合约具有与之前的 `Vesting` 合约相同的功能，另外还增加了一项功能，让用户可以 `preclaim` 部分代币配额，使用户在满足其归属期之前获得有限数量的代币。\r\n\r\n仅使用规范，我们可以创建一个（常规，黑盒） [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/10-vesting-ext/Properties.sol#L27-L29) ，它验证总的提前认领点数始终小于或等于最大可认领点数（这就是用户数量乘以每个用户的最大提前认领点数）：\r\n\r\n    function property_total_preclaimed_lt_eq_max_preclaimable() public view returns(bool result) {\r\n        result = totalPreclaimed <= MAX_PRECLAIMABLE;\r\n    }\r\n    \r\n\r\n这个不变式发现了一个 [中等](https://solodit.xyz/issues/maximum-preclaim-limit-can-be-easily-bypassed-to-preclaim-entire-token-allocation-cyfrin-none-bima-markdown) 严重性漏洞，允许用户提前认领其全部代币配额，而在审计代码的情况下，迅速获得超出其应有的 DAO 投票权。\r\n\r\n##  示例 7 - 操作员注册表腐败\r\n\r\n规范：一个 [`OperatorRegistry`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/11-op-reg/OperatorRegistry.sol) 合约允许用户注册为操作员并接收一个 `operatorId`，其中第一个 `operatorId = 1`，后续的 ID 递增。\r\n\r\n合约存储有多个相互关联的数据结构，使用用户的 `address` 和 `operatorId` 作为映射中的键来相互引用，从而能够通过 `address` 或 `operatorId` 查询操作员数据。用户还可以更新他们的 `address`。\r\n\r\n从这个规范中，我们可以编写一个（常规，黑盒） [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/11-op-reg/Properties.sol#L13-L38) ，它通过确保每个 `operatorId` 与唯一的 `address` 相关来验证这些相互关联的数据结构的数据完整性：\r\n\r\n    EnumerableSet.AddressSet foundAddresses;\r\n    \r\n    function property_operator_ids_have_unique_addresses() public returns(bool result) {\r\n        // 首先从幽灵存储中移除旧的找到的\r\n        uint256 oldFoundLength = foundAddresses.length();\r\n        if(oldFoundLength > 0) {\r\n            address[] memory values = foundAddresses.values();\r\n    \r\n            for(uint256 i; i<oldFoundLength; i++) {\r\n                foundAddresses.remove(values[i]);\r\n            }\r\n        }\r\n    \r\n        // 然后遍历每个当前操作员，获取其地址\r\n        // 并尝试将其添加到找到的集合中。如果添加失败，则为\r\n        // 重复项，违反不变式\r\n        uint128 numOperators = operatorRegistry.numOperators();\r\n        if(numOperators > 0) {\r\n            // 操作员 ID 从 1 开始\r\n            for(uint128 operatorId = 1; operatorId <= numOperators; operatorId++) {\r\n                if(!foundAddresses.add(operatorRegistry.operatorIdToAddress(operatorId))) {\r\n                    return false;\r\n                }\r\n            }\r\n        }\r\n    \r\n        result = true;\r\n    }\r\n    \r\n\r\n这个不变式揭示了一个 [低](https://solodit.xyz/issues/nodeoperatorregistryupdateoperatorcontrollingaddress-allows-to-override-_newoperatoraddress-if-its-address-is-already-assigned-to-an-operator-id-cyfrin-none-cyfrin-swell-barracuda-markdown) 严重性问题，我的队友发现两个不同的 `operatorIds` 可以指向同一个用户 `address` 和相关数据，破坏相互关联的数据结构关系。这在我们的审计中是一个低严重性问题，因为触发腐败的函数是受权限控制的，影响有限，但根据腐败如何被触发和利用，这在其他代码库中可能很容易成为中等或高严重性问题。\r\n\r\n##  示例 8 - 强制清算拒绝服务\r\n\r\n规范：一个 [`LiquidateDos`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/12-liquidate-dos/LiquidateDos.sol) 合约允许交易者进入多个市场并在每个市场中有一个开放头寸。交易者也可以被强制清算：\r\n\r\n*   在确定交易者是否可被清算时，所有开放头寸都会被计算\r\n    \r\n*   如果被清算，则被清算的交易者的所有开放头寸都会关闭\r\n    \r\n*   清算绝不应因意外错误而失败\r\n    \r\n\r\n使用这个规范，我们可以编写一个（常规，白盒）不变式，验证 `liquidate` 函数不会因意外错误而回滚。这个不变式是白盒的，因为它要求我们知道 `liquidate` 的具体实现细节，以便知道哪些错误是预期的。\r\n\r\n在实施 DoS 不变式模糊测试时，有两种方法：\r\n\r\n1.  在 `assertion` 模式下运行 `Echidna` 和 `Medusa`，并在模糊处理程序中有断言，但这在 Foundry 中无法工作\r\n    \r\n2.  有一个 `bool` 幽灵变量，在模糊处理程序中设置，然后将不变式包装在它周围 - 这适用于所有 3 个模糊器\r\n    \r\n\r\n以下是使用第二种实现的 [处理程序](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/12-liquidate-dos/TargetFunctions.sol#L32-L68) 和 [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/11-op-reg/Properties.sol#L13-L38)：\r\n\r\n    // TargetFunctions 模糊处理程序\r\n    function handler_liquidate(uint8 victimIndex) external {\r\n        address victim = _getRandomAddress(victimIndex);\r\n    \r\n        try liquidateDos.liquidate(victim) {\r\n            // 更新幽灵变量\r\n            delete userActiveMarketsCount[victim];\r\n    \r\n            for(uint8 marketId = liquidateDos.MIN_MARKET_ID();\r\n                marketId <= liquidateDos.MAX_MARKET_ID();\r\n                marketId++) {\r\n                delete userActiveMarkets[victim][marketId];\r\n            }\r\n        }\r\n        catch(bytes memory err) {\r\n            bytes4[] memory allowedErrors = new bytes4[](2);\r\n            allowedErrors[0] = ILiquidateDos.LiquidationsDisabled.selector;\r\n            allowedErrors[1] = ILiquidateDos.LiquidateUserNotInAnyMarkets.selector;\r\n    \r\n            if(_isUnexpectedError(bytes4(err), allowedErrors)) {\r\n                liquidateUnexpectedError = true;\r\n            }\r\n        }\r\n    }\r\n    \r\n    // 返回错误是否意外\r\n    function _isUnexpectedError(\r\n        bytes4 errorSelector,\r\n        bytes4[] memory allowedErrors\r\n    ) internal pure returns(bool isUnexpectedError) {\r\n        for (uint256 i; i < allowedErrors.length; i++) {\r\n            if (errorSelector == allowedErrors[i]) {\r\n                return false;\r\n            }\r\n        }\r\n    \r\n        isUnexpectedError = true;\r\n    }\r\n    \r\n    // 属性不变式\r\n    function property_liquidate_no_unexpected_error() public view returns(bool result) {\r\n        result = !liquidateUnexpectedError;\r\n    }\r\n    \r\n\r\n这个不变式发现了一个 [严重](https://solodit.xyz/issues/impossible-to-liquidate-accounts-with-multiple-active-markets-as-liquidationbranchliquidateaccounts-reverts-due-to-corruption-of-ordering-in-tradingaccountactivemarketsids-cyfrin-none-cyfrinzaros-markdown) 严重性漏洞，交易者可以利用这个漏洞使自己无法被清算。\r\n\r\n##  示例 9 - 稳定池排水\r\n\r\n规范：一个 [`StabilityPool`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/13-stability-pool/StabilityPool.sol) 合约，它：\r\n\r\n* 允许用户存入 `debtToken`，用于在清算过程中偿还坏账\r\n\r\n* 作为交换，`debtToken` 存款人从清算过程中扣押的抵押物中获得一部分 `collateralToken` 奖励\r\n\r\n* 包含相当复杂的逻辑来计算 `debtToken` 存款人应获得的奖励份额\r\n\r\n* 必须始终保持偿付能力；池中应始终有足够的 `collateralToken` 来支付应付给 `debtToken` 存款人的奖励\r\n\r\n一个自然从规范中流出的 (常规的黑盒) [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/13-stability-pool/Properties.sol#L9-L23) 是验证池的偿付能力：\r\n\r\n```solidity\r\nfunction property_stability_pool_solvent() public view returns(bool result) {\r\n    uint256 totalClaimableRewards;\r\n\r\n    // 计算每个用户的可领取奖励总额\r\n    for(uint8 i; i<ADDRESS_POOL_LENGTH; i++) {\r\n        address user = addressPool[i];\r\n\r\n        totalClaimableRewards += stabilityPool.getDepositorCollateralGain(user);\r\n    }\r\n\r\n    // 如果可领取的奖励总额小于等于抵押代币余额，则池是偿付的\r\n    if(totalClaimableRewards <= collateralToken.balanceOf(address(stabilityPool)))\r\n        result = true;\r\n}\r\n```\r\n\r\n这个简单的不变式揭示了一种 [致命](https://solodit.xyz/issues/stabilitypoolclaimcollateralgains-should-accrue-depositor-collateral-gains-before-claiming-cyfrin-none-bima-markdown) 漏洞，该漏洞出现在我审计的代码所分叉出来的原始协议中。这个漏洞是通过一个 [“小修复”](https://github.com/prisma-fi/prisma-contracts/commit/76dbc51db0c0d4c92a59776f5effc47e31e88087) 引入的，并在代码库中潜伏了 1 年；它允许一个 `debtToken` 存款人完全抽走 `StabilityPool` 中的所有 `collateralTokens`。\r\n\r\n这个不变式的简单性展示了不变式模糊测试的巨大威力：在不了解复杂的奖励计算代码的情况下，我们可以编写一个简单的黑盒不变式，而模糊测试工具会通过找到一个极其有价值的致命漏洞来破坏它。\r\n\r\n##  示例 10 - 抵押优先级腐败\r\n\r\n规范：一个 [`Priority`](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/src/14-priority/Priority.sol) 合约，用于多抵押贷款协议：\r\n\r\n* 定义抵押物的清算优先级顺序\r\n\r\n* 当发生清算时，风险最高的抵押物会优先清算，以便借款人在清算后剩余的抵押物更加稳定\r\n\r\n* 允许添加和移除抵押物；添加时总是将新抵押物放在优先队列的末尾，而移除时则保留现有顺序，去掉被移除的元素\r\n\r\n从规范中，我们可以编写一个 (常规的黑盒) [不变式](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/14-priority/Properties.sol#L9-L24) 来验证抵押物的顺序始终正确。为了简化我们在模糊测试中的实现，我们使用 4 个抵押物，更新模糊 [处理函数](https://github.com/devdacian/solidity-fuzzing-comparison/blob/main/test/14-priority/TargetFunctions.sol#L10-L46) 中的预期顺序，然后将预期顺序与不变式中的实际顺序进行比较：\r\n\r\n```solidity\r\n// 目标函数模糊处理器更新幽灵变量预期顺序\r\nfunction handler_addCollateral(uint8 collateralId) external {\r\n    collateralId = uint8(between(collateralId,\r\n                                 priority.MIN_COLLATERAL_ID(),\r\n                                 priority.MAX_COLLATERAL_ID()));\r\n\r\n    priority.addCollateral(collateralId);\r\n\r\n    // 更新幽灵变量以反映预期顺序\r\n    if(priority0 == 0) priority0 = collateralId;\r\n    else if(priority1 == 0) priority1 = collateralId;\r\n    else if(priority2 == 0) priority2 = collateralId;\r\n    else priority3 = collateralId;\r\n}\r\n\r\nfunction handler_removeCollateral(uint8 collateralId) external {\r\n    collateralId = uint8(between(collateralId,\r\n                                 priority.MIN_COLLATERAL_ID(),\r\n                                 priority.MAX_COLLATERAL_ID()));\r\n\r\n    priority.removeCollateral(collateralId);\r\n\r\n    // 更新幽灵变量以反映预期顺序\r\n    if(priority0 == collateralId) {\r\n        priority0 = priority1;\r\n        priority1 = priority2;\r\n        priority2 = priority3;\r\n    }\r\n    else if(priority1 == collateralId) {\r\n        priority1 = priority2;\r\n        priority2 = priority3;\r\n    }\r\n    else if(priority2 == collateralId) {\r\n        priority2 = priority3;\r\n    }\r\n\r\n    delete priority3;\r\n}\r\n\r\n// 属性不变式\r\nfunction property_priority_order_correct() public view returns(bool result) {\r\n    if(priority0 != 0) {\r\n        if(priority.getCollateralAtPriority(0) != priority0) return false;\r\n    }\r\n    if(priority1 != 0) {\r\n        if(priority.getCollateralAtPriority(1) != priority1) return false;\r\n    }\r\n    if(priority2 != 0) {\r\n        if(priority.getCollateralAtPriority(2) != priority2) return false;\r\n    }\r\n    if(priority3 != 0) {\r\n        if(priority.getCollateralAtPriority(3) != priority3) return false;\r\n    }\r\n\r\n    result = true;\r\n}\r\n```\r\n\r\n这个不变式揭示了一种 [高](https://solodit.xyz/issues/globalconfigurationremovecollateralfromliquidationpriority-corrupts-the-collateral-priority-order-resulting-in-incorrect-order-of-collateral-liquidation-cyfrin-none-cyfrinzaros-markdown) 漏洞，该漏洞破坏了抵押优先级顺序，导致错误的抵押物被优先清算，结果造成交易者在清算后留下了更不健康的抵押物，从而增加了未来清算的可能性。\r\n\r\n##  结论\r\n\r\n我们回顾了我在真实代码库进行的 9 个简化示例，其中不变式模糊测试本可以被协议开发者“内部”使用，以检测和修复重要漏洞，从而在与外部审计人员合作之前。\r\n\r\n这 9 个不变式中只有 1 个是白盒，这意味着编写它需要理解智能合约的内部实现细节。其他 8 个都是黑盒，可以简单地从协议或合约规范中推导出来。所有 9 个不变式相对都是简单易写和实现的。\r\n\r\n协议开发者和智能合约审计员可以通过学习以不变式思维，且将不变式模糊测试作为他们工作的一部分，显著提高其协议的安全性。\r\n\r\n> 我是 [AI 翻译官](https://learnblockchain.cn/people/19584)，为大家转译优秀英文文章，如有翻译不通的地方，在[这里](https://github.com/lbc-team/Pioneer/blob/master/translations/10147.md)修改，还请包涵～"},"author":{"user":"https://learnblockchain.cn/people/24434","address":null},"history":null,"timestamp":1733368994,"version":1}