Curvance: 不变性释放 - Trail of Bits博客

Nat Chin
2024年4月30日
审计, 区块链, 模糊测试, 不变性开发

欢迎深入了解我们与Curvance共同进行的不变性开发世界。六年来，我们一直在常规代码评审评估中构建不变性，但与Curvance的合作标志着我们首个正式的不变性开发项目，其中我们专注于开发和测试不变性。

在九周的合作中，我们编写并测试了216个不变性，帮助我们发现13个关键问题。我们还找到了显著增强工具的机会，包括高级跟踪打印和语料库保存。这个项目是 navigating 学习曲线和完成技术壮举的旅程，本文将重点介绍我们的协作努力和团队合作在应对挑战中的关键作用。是的，我们也会提到在这个项目中经历的脑细胞测试时刻！

创建高质量的模糊测试套件

模糊测试套件的成功基于其不变性的质量。在整个项目中，我们专注于微调每个不变性的准确性和相关性。模糊测试本质上就像让聪明的猴子在键盘上测试不变性，其有效性 heavily 依赖于它们的精确性。我们与Curvance的九周旅程涉及将代码库属性的深入讨论转化为精确的英语解释，然后将它们编码为可执行测试，如下面的截图所示。

从一开始，Curvance的Chris经常可用，帮助澄清代码的预期行为并解释Curvance的设计选择。他的见解总是澄清复杂的功能和行为，他总是帮助进行动手调试和检查我们的不变性。这次合作之所以如此富有成效，得益于Chris的持续反馈和全程与我们并肩工作。谢谢Curvance！

我们成功背后的工具（和支持团队）

除了Curvance的参与，我们内部团队对Echidna、Medusa和CloudExec的支持也帮助我们的项目成功。他们对问题的快速响应，特别是在广泛的重基和复杂调试期间，至关重要。Curvance的合作将这些工具推到了极限，我们为应对挑战而必须想出的解决方案导致了这些工具的重大增强。

CloudExec在将长时模糊测试作业部署到DigitalOcean上证明是无价的。我们将其与Echidna和Medusa集成以进行 prolonged 运行，使Curvance能够轻松设置自己未来的模糊测试运行。我们 pinpointed CloudExec的改进领域，如其输出数据的保存，您可以在其GitHub问题跟踪器上看到。我们已经解决了许多这些问题。

Echidna，我们基于属性的Ethereum合约模糊测试器，在 falsifying 断言方面至关重要。我们首先在探索模式下使用Echidna广泛覆盖Curvance代码库，然后进入断言模式，使用从1000万到1000亿次迭代。在我们九周的合作中，Echidna的密集使用帮助我们发现了工具的关键改进领域，使其更容易调试和保留 explored 代码区域的状态。

Medusa，我们基于geth的实验性模糊测试器，在覆盖努力中 complement Echidna，以 falsifying Curvance上的不变性。在我们能使用Medusa进行这次合作之前，我们需要修复一个已知的内存不足错误。这个错误的修复——以及在CloudExec中实施的修复以帮助其更好地保存输出数据—— critically 改进了工具，并帮助最大化我们对Curvance代码的覆盖。它开始运行后立即发现了一个中等严重性的错误，而Echidna错过了。（Echidna最终在我们更改块时间延迟后找到了这个错误， likely 由于模糊测试器的非确定性。）

漫长而曲折的道路

尽管我们有工具团队和客户的最佳支持，我们在整个项目中仍然面临相当大的挑战——从需要跟上Curvance的持续开发，到调试断言失败的挑战。但通过应对这些挑战，我们学到了关于不变性开发性质的重要教训，并能够实施对我们工具的关键升级以改进我们的整体过程。

竞速跟上Curvance的代码变化

Curvance代码库的变化——如函数移除、函数参数添加、参数和错误消息调整，以及源合约重命名——经常通过使现有不变性无效或导致一系列断言失败来挑战我们的模糊测试套件。最终，这些变化使我们的现有语料库项过时和不可用，我们必须 constantly 重基我们的模糊测试套件并修订现有和新的不变性，以确保它们与 evolving 系统的持续相关性。这个迭代过程与客户的代码开发并行，呈现了真阳性（客户代码中的实际错误）和假阳性（由于不正确或过时的不变性导致的失败）的混合。这样的结果强调了模糊测试不是静态的、一次性的设置；它需要持续的维护和更新，类似于任何活跃代码库的开发。

理解每次重基后不变性变化背后的 rationale 至关重要。没有 fully 掌握其含义的草率调整可能 inadvertently 掩盖错误，削弱模糊测试套件的有效性。保持套件的活跃和相关性与代码库的开发本身一样重要。这不仅仅是让模糊测试器运行；而是保持它与测试系统的对齐。记住，模糊测试套件的真正力量在于其不变性的准确性。

关键工具升级和学到的教训

在提交a96dc9a中Lendtroller合约名称更改为MarketManager后，我们必须进行 significant 重基。这个变化 drastically 影响了我们的工作，因为Echidna刚刚使用CloudExec在云中完成了43天的运行。这个 nonstop 执行允许Echidna开发一个详细的语料库，能够 autonomously 处理复杂清算。不幸的是，这个变化使这个语料库过时，每个语料库项导致Echidna工作线程在事务重放时崩溃。随着我们15个工作线程的设置，只需要14个更多无法重放的事务，所有Echidna工作线程就会崩溃，完全停止Echidna：

由于Curvance的代码变化，我们的重基导致了一个 significant 问题：我们的模糊测试器无法再访问探索复杂状态所需的MarketManager功能，如发布抵押和借入债务。这个问题 prompt 我们对Echidna进行关键更新， specifically 增强其验证和重放语料库序列而不崩溃的能力。我们还对Medusa进行了更新，以改进其跟踪语料库健康和修复启动恐慌的能力。关于维护动态语料库的扩展讨论 ensued，我们的工程总监介入手动调整语料库，提供了一些缓解。

我们调整策略以适应新代码库缺乏覆盖的情况。我们为合约名称更改前的代码库版本开发了清算特定的不变性，同时在 different 模式下运行更新版本以提升覆盖。CloudExec的新功能，如命名作业、改进的输出目录检查点和失败作业的检查点，在区分和管理这些运行中 key。尽管所有这些改进，我们放弃了旧语料库，并选择将设置功能集成到关键合约中以加速覆盖。虽然在增加覆盖方面有效，但这个策略引入了偏见，特别是在清算场景中，通过依赖静态值。这个限制，在代码库中用/// @coverage:limitation标签标记， underscores 在我们的有状态测试中扩大输入范围以确保全面系统探索的重要性。

试验和磨难：调试

Curvance不变性开发报告主要 highlight 我们调试的结果，而没有深入探讨这些发现背后的复杂调查和根本原因分析旅程。这个过程的一部分，涉及一旦断言失败被识别后的详细分析，需要 significant 努力。

我们的主要挑战是剖析长调用序列，通常范围从9到70个事务，需要深入 scrutiny 以识别错误和意外值 crept in 的地方。一些序列跨越 up to 2900万个块或包括超过6年的时间延迟，为我们的系统行为理解添加了复杂性层。为了解决这个问题，我们必须手动插入日志以获取详细状态信息，将调试变成 exhaustive 和手动努力：

我们手动缩小事务序列的能力 hinged 于我们对Curvance系统的深入理解。这个详细知识对我们有效识别哪些事务对 uncovering 漏洞 essential 和哪些可以丢弃至关重要。随着我们在整个项目中获得对系统的 deeper 洞察，我们 streamline 事务序列的能力 markedly 改进。

基于我们梳理事务序列的工作，我们在Echidna中实施了一个丰富的重现器跟踪功能，提供我们执行期间系统的详细跟踪和事务失败序列每一步系统状态的 elaborate 打印输出。同时，我们还向Medusa添加了事务序列的缩小限制以修复间歇性断言失败，并更新了Medusa的覆盖报告以增加其可读性。这些更新后Echidna跟踪打印的 stark 差异可以在下图中 easily 看到：

最后，我们基于我们合作期间的大多数断言失败创建了相应的单元测试。最初，将失败转换为单元测试是手动和耗时的，但到最后，我们 streamline 过程只需半小时。我们使用从这个经验中获得的见解开发了fuzz-utils，一个将断言失败自动转换为单元测试的工具。虽然尚未 extensively 测试，但其对未来合作的潜力 excites 我们！

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

在Curvance代码库的 significant 变化后，我们遇到了一个令人困惑的断言失败。最初，我们怀疑它可能是一个假阳性，这在主要代码变化中常见。然而，在检查Curvance源代码的变化后，根本原因并不 immediately 明显， leading 我们进入一个复杂和彻底的调试过程。

我们分析了Echidna中的完整重现器跟踪（一个在这次合作中添加的Echidna功能，如前一节所述），并在 different 发送者上测试了假设。我们 crafted 并执行了一系列单元测试，每次迭代 shed 更多 light 于底层机制。是时候 zoom out 以识别涉及新断言失败的功能中的共性， leading 我们专注于processExpiredLock函数。通过 closely 审查这个函数，我们发现了一个重要的断言缺失：确保在调用带有“relock”选项的函数后用户锁的数量保持不变。

当我们重新运行模糊测试器时，它 immediately 揭示了错误：这样的调用会处理过期的锁但 incorrectly 授予用户一个新锁而不移除旧锁，导致锁总数意外增加。这在combineAllLocks函数中导致所有形式的问题：合约总是认为用户比实际多一个锁。Eureka！

这个跟踪显示处理过期锁后用户锁数量的增加：

使这个发现 particularly striking 的是它能够 elude 通过各种安全评审和测试的检测。单元测试，结果发现，正在检查一个不正确的后条件，在其检查中 conceal 错误， masking 其错误在测试套件内。这个代码库上的无状态模糊测试测试（由Curvance在这次合作前构建）实际上在这个错误修复后开始失败。这 highlighted 不仅需要复杂和 meticulous 测试验证代码库的每个方面，而且需要 continually 质疑和验证目标代码的每个方面——及其测试。

下一步是什么？

反思我们与Curvance的旅程，我们认识到 comprehensive 安全工具包对智能合约的重要性，包括单元、集成和模糊测试，以 uncover 系统复杂性和潜在问题。我们过去九周的合作允许我们 meticulously 检查和理解系统，增强我们发现的准确性并深化我们相互的知识。与Curvance紧密合作证明在揭示技术 intricacies 方面 crucial， leading 开发一个有状态模糊测试套件，将随着代码 evolve 和扩展，确保持续的安全和洞察。

如果您正在开发一个项目并想探索有状态模糊测试，我们很乐意与您聊天！

如果您喜欢这篇文章，分享它：
Twitter
LinkedIn
GitHub
Mastodon
Hacker News

页面内容
创建高质量的模糊测试套件
我们成功背后的工具（和支持团队）
漫长而曲折的道路
竞速跟上Curvance的代码变化
试验和磨难：调试
下一步是什么？
最近帖子
用Deptective调查您的依赖项
系好安全带，Buttercup，AIxCC的评分回合正在进行中！
使您的智能合约成熟超越私钥风险
Go解析器中意外的安全脚枪
我们从审查Silence Laboratories的首批DKLs23库中学到了什么
© 2025 Trail of Bits。
使用Hugo和Mainroad主题生成。