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