Curvance：不变式开发的突破之旅
欢迎深入了解我们与Curvance合作的不变式开发世界。六年来，我们一直在常规代码评审评估中构建不变式，但Curvance项目标志着我们首个正式的不变式开发项目，全程专注于不变式的开发与测试。
在九周的合作中，我们编写并测试了216个不变式，帮助发现了13个关键问题。我们还找到了大幅改进工具的机会，包括高级跟踪打印和语料库保存。该项目是一次攀登学习曲线并实现技术壮举的旅程，本文将重点介绍我们的协作努力以及团队合作在应对挑战中的关键作用。当然，我们也会谈及项目中那些“烧脑”的时刻！
创建高质量的模糊测试套件
模糊测试套件的成功基于其不变式的质量。在整个项目中，我们专注于微调每个不变式的准确性和相关性。模糊测试本质上就像让聪明的猴子在键盘上测试不变式，其效果高度依赖于它们的精确性。我们与Curvance的九周合作涉及将代码库属性的深入讨论转化为精确的英文解释，然后编码成可执行测试，如下截图所示。
从一开始，Curvance的Chris就经常帮助我们澄清代码的预期行为并解释Curvance的设计选择。他的见解总是澄清复杂函数和行为，他还总是帮助进行实际调试和检查我们的不变式。这次合作如此富有成效，得益于Chris的持续反馈和全程与我们并肩工作。谢谢Curvance！
成功背后的工具（和支持团队）
除了Curvance的参与，我们内部Echidna、Medusa和CloudExec团队的支持也帮助项目成功。他们对问题的快速响应，尤其是在大规模重基和复杂调试期间，至关重要。Curvance项目将这些工具推向了极限，我们为应对挑战想出的解决方案导致了这些工具的重大改进。
CloudExec在将长时间模糊测试任务部署到DigitalOcean上证明是无价的。我们将其与Echidna和Medusa集成进行长时间运行，使Curvance能够轻松设置自己未来的模糊测试运行。我们指出了CloudExec的改进领域，如其输出数据的保存，您可以在其GitHub问题跟踪器上看到。我们已经解决了许多这些问题。
Echidna，我们基于属性的Ethereum合约模糊测试器，在证伪断言中至关重要。我们首先在探索模式下使用Echidna广泛覆盖Curvance代码库，然后进入断言模式，使用从1000万到1000亿次迭代。在九周合作中密集使用Echidna帮助我们发现了工具的关键改进领域，使其更容易调试和保留探索代码区域的状态。
Medusa，我们基于geth的实验性模糊测试器，在证伪Curvance不变式的覆盖努力中补充了Echidna。在我们能使用Medusa进行这次合作之前，我们需要修复一个已知的内存不足错误。这个错误的修复——以及在CloudExec中实施的修复以帮助其更好地保存输出数据——关键改进了工具，并帮助最大化我们对Curvance代码的覆盖。它开始运行后立即发现了代码中一个中等严重性的错误，Echidna错过了。（Echidna最终在我们更改块时间延迟后找到了这个错误，可能由于模糊测试器的非确定性。）
漫长而曲折的道路
尽管我们有工具团队和客户所能提供的最佳支持，我们在整个项目中仍面临相当大的挑战——从需要跟上Curvance的持续开发，到调试断言失败的挑战。但通过应对这些挑战，我们学到了关于不变式开发本质的重要教训，并能够实施对我们工具的关键升级以改进整体流程。
竞速跟上Curvance的代码变更
Curvance代码库的变更——如函数移除、函数参数添加、参数和错误消息调整，以及源合约重命名——经常通过使现有不变式无效或导致一系列断言失败来挑战我们的模糊测试套件。最终，这些变更使我们现有的语料库项过时且不可用，我们必须不断重基我们的模糊测试套件并修订现有和新的不变式，以确保它们与 evolving 系统的持续相关性。这个迭代过程与客户的代码开发并行，呈现了真阳性（客户代码中的实际错误）和假阳性（由于不正确或过时的不变式导致的失败）的混合。这样的结果强调模糊测试不是静态的一次性设置；它需要持续维护和更新，类似于任何活跃代码库的开发。
理解每次重基后不变式变更背后的原理至关重要。没有完全掌握其含义就匆忙调整可能无意中掩盖错误，削弱模糊测试套件的有效性。保持套件的活跃和相关性与代码库的开发本身同样重要。这不仅仅是让模糊测试器运行；而是保持其与测试系统的对齐。记住，模糊测试套件的真正力量在于其不变式的准确性。
关键工具升级和经验教训
在提交a96dc9a中将Lendtroller合约名称更改为MarketManager后，我们必须进行重大重基。这个变更极大地影响了我们的工作，因为Echidna刚刚使用CloudExec在云端运行了43天。这个不间断执行使Echidna能够开发一个详细的语料库，能够自主处理复杂清算。不幸的是，变更使这个语料库过时，每个语料库项导致Echidna工作线程在交易重放时崩溃。在我们的15个工作线程设置中，只需要14个更多无法重放的交易就使所有Echidna工作线程崩溃，完全停止Echidna：
由于Curvance的代码变更，我们的重基导致了一个重大问题：我们的模糊测试器无法再访问探索复杂状态所需的MarketManager函数，如发布抵押和借入债务。这个问题促使我们对Echidna进行关键更新，特别是增强其验证和重放语料库序列而不崩溃的能力。我们还对Medusa进行了更新，以改进其跟踪语料库健康和修复启动恐慌的能力。关于维护动态语料库的扩展讨论随之而来，我们的工程总监介入手动调整语料库，提供了一些缓解。
我们调整策略以适应新代码库缺乏覆盖的情况。我们为合约名称变更前的代码库版本开发了特定于清算的不变式，同时在不同模式下运行更新版本以提升覆盖。CloudExec的新功能，如命名作业、改进的输出目录检查点，以及失败作业的检查点，在区分和管理这些运行中至关重要。尽管有所有这些改进，我们放弃了旧语料库，并选择将设置函数集成到关键合约中以加速覆盖。虽然有效增加覆盖，但这个策略引入了偏见，尤其是在清算场景中，通过依赖静态值。这个限制，在代码库中用/// @coverage:limitation标签标记，强调了在我们有状态测试中扩大输入范围以确保全面系统探索的重要性。
试验和磨难：调试
Curvance不变式开发报告主要突出了我们调试的结果，而没有深入探讨这些发现背后的复杂调查和根本原因分析旅程。过程的这一部分，涉及一旦识别断言失败后的详细分析，需要大量努力。
我们的主要挑战是剖析长调用序列，通常范围从9到70个交易，需要深入审查以识别错误和意外值出现的地方。一些序列跨越高达2900万个块或包括超过6年的时间延迟，为我们理解系统行为增加了复杂性层。为了解决这个问题，我们必须手动插入日志以获取详细状态信息，将调试变成详尽的手动努力：
我们手动缩小交易序列的能力取决于我们对Curvance系统的深入理解。这个详细知识对我们有效识别哪些交易对 uncovering 漏洞至关重要，哪些可以丢弃至关重要。随着我们在整个项目中获得对系统的更深洞察，我们精简交易序列的能力显著提高。
基于我们梳理交易序列的工作，我们在Echidna中实施了一个丰富的重现器跟踪功能，提供我们执行期间系统的详细跟踪和交易失败序列每一步系统状态的详细打印。同时，我们还向Medusa添加了交易序列的缩小限制以修复间歇性断言失败，并更新了Medusa的覆盖报告以增加其可读性。这些更新后Echidna跟踪打印的鲜明差异可以在下图中轻松看到：
最后，我们基于合作期间大多数断言失败创建了相应的单元测试。最初，将失败转换为单元测试是手动且耗时的，但到最后，我们精简了过程到只需半小时。我们利用从这次经验中获得的洞察开发了fuzz-utils，一个将断言失败自动转换为单元测试的工具。虽然尚未广泛测试，但其对未来合作的潜力令我们兴奋！
一个锁太多：TOB-CURV-4背后的故事
在Curvance代码库的重大变更后，我们遇到了一个令人困惑的断言失败。最初，我们怀疑它可能是假阳性，重大代码变更中常见。然而，在检查Curvance源代码的变更后，根本原因并不立即明显，导致我们进入一个复杂而彻底的调试过程。
我们分析了Echidna中的完整重现器跟踪（一个在这次合作中添加的Echidna功能，如前一节所述），并在不同发送者上测试了假设。我们精心制作并执行了一系列单元测试，每次迭代都更深入揭示底层机制。是时候放大以识别新断言失败中涉及函数的共性， leading us to focus on the processExpiredLock function。通过仔细审查这个函数，我们发现了一个重要断言缺失：确保在调用带有“relock”选项的函数后用户锁数量保持不变。
当我们重新运行模糊测试器时，它立即揭示了错误：这样的调用会处理过期锁但错误地授予用户一个新锁而不移除旧锁，导致锁总数意外增加。这在combineAllLocks函数中导致了各种问题：合约总是认为用户比实际多一个锁。Eureka！
这个跟踪显示了处理过期锁后用户锁数量的增加：
这个发现特别引人注目的是其能够通过各种安全评审和测试逃避检测。单元测试，结果发现，正在检查不正确的后条件，在其检查中隐藏错误，在测试套件中掩盖其错误。这个代码库上的无状态模糊测试测试（由Curvance在这次合作前构建）实际上在这个错误修复后开始失败。这突出了不仅需要复杂和细致的测试来验证代码库的每个方面，而且需要持续质疑和验证目标代码及其测试的每个方面的必要性。
下一步是什么？
反思我们与Curvance的旅程，我们认识到全面安全工具包对智能合约的重要性，包括单元、集成和模糊测试，以 uncover 系统复杂性和潜在问题。过去九周的合作使我们能够细致检查并理解系统，增强我们发现的准确性并深化我们相互的知识。与Curvance紧密合作证明在揭示技术 intricacies 中至关重要， leading to the development of a stateful fuzzing suite that will evolve and expand with the code, ensuring continued security and insights.
如果您正在开发一个项目并想探索有状态模糊测试，我们很乐意与您聊天！
如果您喜欢这篇文章，分享它： Twitter LinkedIn GitHub Mastodon Hacker News