对 Badger DAO 的 eBTC 协议进行为期 6 周模糊测试的经验总结

更多来自 “一切皆可Fuzz” 的内容

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

已经有账户了？ 登录

从对 Badger DAO 的 eBTC 协议进行 6 周的 Fuzzing 中学到的

来自全面的形式化规范和不变性测试审计的主要收获和最佳实践

注意：这篇文章最初发布在这里。

概述

在六周的时间里，我有机会与 Badger DAO 合作，以增强其 eBTC 协议的不变性测试。在此期间，我们建立并实施了 40 多项属性，验证了 Spearbit 手动审查的发现，并发现了之前未公开的 bug。这些问题已由团队解决，团队进一步实施了持续的 fuzzing 集成，以监控代码更改后被破坏的不变性。

在本文中，我将分享我们从这次全面的形式化规范和不变性测试审计中的主要收获和最佳实践。

eBTC 简介

eBTC 是一种抵押加密资产，软锚定于比特币的价格，并建立在以太坊网络上。它完全由 Lido Staked ETH (stETH) 支持，并建立在 Liquity 的 LUSD 模型之上，以维持其Hook稳定性。用户通过将 stETH 存入协议来创建抵押债务头寸 (CDP)，这允许他们铸造 eBTC，然后可以在 DeFi 中使用并兑换回 stETH。

主要收获

1. Echidna 仍然是这项工作的最佳工具

在开始一个 fuzzing 项目时，我们经常会问自己应该选择哪个工具。虽然理论上你可以构建一个 与 fuzzer 无关的合约，但实际上，目标合约的断言方法和整体结构在某种程度上是程序相关的，这使得选择一个程序并坚持使用它更容易。

在整个项目中，我们评估了 Echidna、Foundry 和 Medusa，认为它们是 Solidity 智能合约最有前途的三种开源 fuzzer。

尽管一些 benchmarks 显示 Foundry 和 Medusa 在某些情况下可能比 Echidna 更快，但 Foundry 缺少 不变性测试的覆盖率报告 以及 Medusa 处于初始阶段的序列收缩是状态 fuzzing 的一大退步。

事实上，应用于现有代码库的一些最具影响力的重构只有在分析了某些代码路径甚至没有被 fuzzer 命中的情况下才成为可能。

只有在达到 100% 的行覆盖率后，我们才能最终开始打破一些不变性并发现错误，并且只有通过简短、可重现的测试，我们才能正确理解问题的根本原因。如果没有这两个关键特性，我们建议将 Foundry 和 Medusa 与 Echidna 一起使用，而不是完全替代。

2. 使用测试转换器加速调试过程

fuzz 测试的最大挑战之一是理解发生了什么。

在 fuzzer 将不同的值抛向你的合约并且你执行多个 bound 或 clampBetween 函数以限制目标函数中的随机输入之后，甚至更难理解初始输入与合约的最终状态之间的确切关系。

我们没有发出事件（这是官方推荐的方法 用于调试失败属性）或使用调用摘要（另一种调试方法，通常在 Foundry 不变性测试中使用），我们提出了一种新的方法：创建测试转换器。

测试转换器是一个辅助测试合约，EchidnaToFoundry.t.sol，其创建的唯一目的是从“Echidna 序列”转换为“Foundry 单元测试”。

此文件包含一个与 Echidna 具有相同目标函数的合约，用于从“随机输入”转换回“硬编码输入”。因此，我们有非常小的单元测试，这允许我们扩展、集成到测试套件中，并通过检查其他状态变量更轻松地进行调试。此外，最重要的是，它避免了向 Echidna 的目标合约添加事件的过程，这通常意味着一遍又一遍地运行该工具直到找到错误。

通过适当的代码分隔，可以直接从 Echidna 合约中提取此测试转换器。因此，在你开始 fuzzing 活动时，请提前考虑并进行相应的计划。一个重要的注意事项是，测试设置应在 Foundry 和 Echidna 之间保持一致，包括初始余额，以便你可以轻松地将 Echidna 运行的最终状态与 Foundry 的最终状态进行比较。

3. 利用现有工具来加快设置时间

尽管状态不变性测试具有明显的优势，但设置环境的摩擦明显高于简单的 Foundry fuzz 测试。这就是为什么要利用现有工具来加快此过程的原因。

一个有用的工具是 Trail of Bit 的 @crytic/properties 存储库，它可以帮助创建 echidna 测试，它带有有用的辅助函数和常见 ERC 标准的预构建属性。

在此项目过程中，我们扩展了存储库，其中包含其他辅助合约、Dockerfile 和其他样板代码，希望这能使新项目更容易引导其不变性测试。

Badger DAO 即将举办一场 Code4rena 竞赛，之后人们将被邀请 fork 其不变性并破坏代码，因此请留意 Bug Bounty 计划的启动，该计划将授予对其不变性测试设置的访问权限。

4. 注意简化假设中的隐含偏差

在我们的参与过程中，我们多次遇到难以理解的测试用例。为了更好地理解它们为何失败，我们采用了一些简化假设。但是，这并不总是被证明是最佳策略，因为它有时会将根本原因隐藏在假阴性之后：

4.1. 小心简化的值

虽然 “漂亮的值” 使重现 bug 变得更容易，但它们可能会掩盖现实世界中的问题。例如，在分析与抵押品和债务值相关的会计不变性时，我们最初忽略了 stETH 重新调整，并将价值 1 美元的抵押品视为等于价值 1 美元的债务，旨在精确计算这些数量的美元价值。

这种方法允许在电子表格上分析时进行简单的计算和易于理解的值。但是，当 fuzzer 再次开始测试时，它会立即崩溃。

经过广泛的调试后，我们意识到我们的简化假设导致我们的公式失败，要么是因为错过了重新调整或价格转换，要么是因为缺少除法或乘以一个常数因子。最终，我们花费了大量时间来调试我们简单的方程式，并让我们意识到这种策略毕竟不是最有效的。

4.2. 当从测试中排除功能时要小心

当系统有多个公共/外部函数作为入口点时，减少目标函数的数量可能很诱人，尤其是当它们提供类似功能时。但是，根据这些函数的内部结构，仅依赖其中一个而不是另一个可能会向 fuzzer 隐藏关键 bug。

一个典型的例子是与 CDP 清算相关的 bug，该 bug 仅在会清算随机 CDP 的函数中发现，但不会触发旨在按 ICR 顺序清算 CDP 的类似函数。

4.3 避免必须始终成立的不变性的假阴性

使用 require 检查（或 vm.assume）也可能引入假阴性，尤其是在你定位必须始终成立的不变性时。

例如，如果你的不变性期望特定事务在特定条件下永远不会失败，那么你还需要确保不存在失败案例。通过仅测试happy path，你可能会忽略潜在的拒绝服务问题，否则可能会违反你的不变性。

5. 尽可能在数学上证明你的不变性

有时，不变性可能会一直被破坏，因为你认为它是真的，但你还没有彻底证明它的正确性。在这种情况下，最好写下代表该不变性的数学方程式，并尝试证明它适用于所有情况。

其中一个案例是 “TCR 必须在清算后增加” 不变性。我们认为它在所有情况下都成立，但在重新分配期间，它在数学上被证明是无效的。具体来说，在涉及不良债务重新分配的清算期间，清算人索取抵押品后，CDP 的一部分债务保留在系统中，这可能会进一步降低 TCR。

这是一个预期的行为，而不是问题，但它说明了不变性与我们最初设想的并不完全一致。

结论

与 Badger DAO 的团队合作，尤其是 @GalloDaSballo 和 @dapp_whisperer，是一次充满学习的经历。他们对安全性的重视是无与伦比的，他们在审查、调试和分类假阳性方面的耐心为这次参与的成功做出了巨大贡献。

安全审查，尤其是对于像金融协议这样关键的协议，在区块链世界中至关重要。这次参与不仅加强了这种方法的优势，而且还提供了有关优化测试过程的宝贵见解。

如果你想讨论不变性测试策略，请不要犹豫与我联系。

• 原文链接： allthingsfuzzy.substack....
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～