Curvance：不变性释放——Trail of Bits博客

作者：Nat Chin
发布日期：2024年4月30日
标签：审计, 区块链, 模糊测试, 不变性开发

欢迎深入探索我们与Curvance共同进行的不变性开发世界。六年来我们一直在常规代码评审中构建不变性，但Curvance项目是首个正式的不变性开发项目，全程专注于不变性的开发与测试。

在九周的合作中，我们编写并测试了216个不变性，发现了13个关键问题。同时我们改进了工具链，包括高级追踪打印和语料库保存功能。本项目经历了技术挑战与突破，本文将重点展示团队协作如何助力我们应对挑战，并分享项目中“烧脑”的瞬间！

构建高质量模糊测试套件

模糊测试套件的成功取决于不变性的质量。本项目我们专注于优化每个不变性的准确性与相关性。模糊测试本质是让“智能猴子”敲键盘测试不变性，其效果高度依赖测试精度。九周内我们将代码库特性的深度讨论转化为精确的英文描述，再编码为可执行测试，如下图所示：

Curvance的Chris全程协助厘清代码预期行为并解释设计决策。他的洞察力始终能澄清复杂功能，并亲自参与调试和不变性检查。项目的成功离不开Chris的持续反馈和并肩作战。感谢Curvance团队！

成功背后的工具（与支持团队）

除Curvance外，Echidna、Medusa和CloudExec内部团队的支持至关重要。他们对问题的快速响应（尤其在重大重构和复杂调试时）是项目成功的关键。本项目将这些工具推向极限，我们为应对挑战提出的解决方案显著增强了工具能力。

CloudExec在DigitalOcean部署长时模糊测试任务中价值巨大。我们将其与Echidna/Medusa集成实现持续运行，使Curvance能轻松设置未来测试。我们明确了CloudExec的改进点（如输出数据保存），已在GitHub问题跟踪器中处理多数问题。

Echidna（基于属性的以太坊合约模糊测试器）在证伪断言中发挥核心作用。我们先在探索模式广泛覆盖代码库，后转入断言模式（迭代次数从1000万到1000亿次）。九周的高强度使用帮助我们发现了工具的关键改进点，使其更易调试并保持代码探索状态。

Medusa（基于geth的实验性模糊测试器）与Echidna协同覆盖Curvance不变性证伪。使用前我们修复了已知内存溢出错误。该修复（与CloudExec输出数据保存改进共同）显著提升工具能力，最大化代码覆盖率。启动后立即发现Echidna遗漏的中危漏洞（修改区块时间延迟后Echidna也发现该漏洞，可能因模糊测试非确定性）。

曲折前行之路

尽管有工具团队和客户的最佳支持，我们仍面临重大挑战：追赶Curvance持续开发、调试断言失败等。应对这些挑战让我们深刻理解不变性开发本质，并实现对工具的关键升级。

追赶Curvance代码变更

代码库变更（如函数删除/参数添加/参数调整/源合约重命名）常使现有不变性失效或引发断言失败链，导致语料项过时。我们不得不持续重构测试套件并修订新旧不变性以保持与演进系统的相关性。此迭代过程伴随客户代码开发，混合了真阳性（代码真实错误）和假阳性（错误/过时不变性导致）。结果表明模糊测试非一次性静态设置，而需像活跃代码库一样持续维护。

理解每次重构后不变性变更的原理至关重要。未充分理解影响就匆忙调整可能掩盖错误，削弱测试套件效果。保持套件活力与代码库开发同等重要——不仅是运行测试，更是维持与受测系统的对齐。记住：模糊测试套件的真正力量在于不变性的准确性。

关键工具升级与经验总结

a96dc9a提交将Lendtroller合约重命名为MarketManager后，我们进行了重大重构。此变更严重影响工作：Echidna刚完成43天CloudExec云端运行，已建立能自主处理复杂清算的详细语料库。但变更使语料库过时，每个语料项导致Echidna工作线程在交易回放时崩溃。15个工作线程仅需14个无法回放的交易就会全部崩溃，彻底中止Echidna：

重构导致模糊测试器无法访问探索复杂状态所需的MarketManager功能（如提交抵押和借款）。这促使我们对Echidna进行关键更新，增强其验证和回放语料序列能力而不崩溃。同时更新Medusa以改进语料健康跟踪和启动恐慌修复。经延长讨论后，工程总监手动调整语料库以缓解问题。

我们调整策略应对新代码库覆盖率不足：为合约更名前的版本开发清算专用不变性，同时以不同模式运行更新版本以提高覆盖率。CloudExec的新功能（如命名作业、输出目录检查点、失败作业检查点）是区分和管理这些运行的关键。尽管有改进，我们放弃了旧语料库，选择将设置函数集成到关键合约以加速覆盖。此策略虽有效但引入偏差（尤其在清算场景中依赖静态值）。代码库中的/// @coverage:limitation标签标明了该限制，强调需在状态测试中扩大输入范围以确保全面系统探索。

试炼与磨难：调试

Curvance不变性开发报告主要突出调试结果，未深入调查和根本原因分析的复杂过程。此部分需在识别断言失败后投入大量精力进行详细分析。

主要挑战是解析长调用序列（常含9-70笔交易），需深入审查以识别错误和意外值出现位置。部分序列跨越2900万个区块或包含超6年时间延迟，增加了理解系统行为的复杂性。为此我们手动插入日志获取详细状态信息，使调试成为 exhaustive 手动任务：

手动收缩交易序列的能力依赖于对Curvance系统的深入理解。此知识对我们有效识别哪些交易对发现漏洞关键、哪些可丢弃至关重要。随着项目深入，我们精简交易序列的能力显著提升。

基于交易序列梳理工作，我们在Echidna中实现了丰富重现器追踪功能，提供执行期间系统详细追踪和交易失败序列每步的系统状态打印。同时为Medusa添加交易序列收缩限制以修复间歇性断言失败，并更新覆盖率报告增强可读性。更新后Echidna追踪打印的显著差异见下图：

最后我们基于多数断言失败创建了对应单元测试。初始转换失败为单元测试耗时费力，但最终流程精简至半小时。利用此经验我们开发了fuzz-utils（将断言失败自动转换为单元测试的工具）。虽尚未广泛测试，但其在未来项目中的潜力令人兴奋！

多一把锁：TOB-CURV-4背后的故事

Curvance代码库重大变更后，我们遇到令人困惑的断言失败。初始怀疑是假阳性（大变更常见现象），但检查源代码后根本原因不明，进入复杂彻底的调试过程。

我们分析了Echidna中的完整重现器追踪（本项目新增功能），测试了不同发送者的假设。设计并执行一系列单元测试，每次迭代更清晰揭示底层机制。需要 zoom out 识别新断言失败中涉及函数的共性，最终聚焦于processExpiredLock函数。仔细审查后发现缺少关键断言：确保调用"relock"选项后用户锁数量不变。

重运行模糊测试器立即显示错误：此类调用会处理过期锁但错误授予用户新锁而未移除旧锁，导致锁总数意外增加。这在combineAllLocks函数中引发各种问题：合约总认为用户比实际多一把锁。Eureka！

用户锁增加追踪（完整不变性开发报告TOB-CURV-4发现中提供）

此发现突出之处在于其能逃过多种安全评审和测试检测。单元测试原来在检查错误后条件，在检查中隐藏了错误。代码库的无状态模糊测试（本项目前由Curvance构建）在修复此错误后开始失败。这强调不仅需要复杂细致测试验证代码库每个方面，还需持续质疑和验证目标代码及其测试的每个方面。

下一步？

回顾Curvance之旅，我们认识到智能合约全面安全工具包（含单元/集成/模糊测试）对发现系统复杂性和潜在问题的重要性。过去九周合作让我们细致检查并理解系统，提升发现准确性并深化双方知识。与Curvance紧密合作对揭示技术复杂性至关重要，导致开发出随代码演进的状态模糊测试套件，确保持续安全与洞察。

如果您在开发项目并想探索状态模糊测试，我们乐意交流！

如果您喜欢本文，请分享至：
Twitter | LinkedIn | GitHub | Mastodon | Hacker News

页面内容：
构建高质量模糊测试套件
成功背后的工具（与支持团队）
曲折前行之路
追赶Curvance代码变更
试炼与磨难：调试
下一步？
近期文章
非传统创新者奖学金
劫持您的PajaMAS中的多智能体系统
我们构建了MCP始终需要的安全层
废弃硬件中的零日漏洞利用
Inside EthCC[8]：成为智能合约审计师
© 2025 Trail of Bits.
使用Hugo和Mainroad主题生成。