Curvance: 不变式全面释放 - Trail of Bits博客

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

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

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

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

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

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

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

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

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

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

漫长而曲折的道路

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

竞速跟上Curvance的代码变化

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

理解每次重构后不变式变化背后的原理至关重要。在没有完全掌握其含义的情况下匆忙调整可能会无意中掩盖错误，削弱模糊测试套件的有效性。保持套件的活跃性和相关性与代码库的开发本身同样重要。这不仅仅是让模糊测试器运行；而是保持它与测试系统的对齐。记住，模糊测试套件的真正力量在于其不变式的准确性。

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

在提交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系统的深入理解。这些详细知识对我们有效识别哪些交易对发现漏洞至关重要，哪些可以丢弃至关重要。随着我们在整个项目中获得对系统的更深入洞察，我们精简交易序列的能力显著提高。

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

最后，我们根据我们合作期间的大多数断言失败创建了相应的单元测试。最初，将失败转换为单元测试是手动且耗时的，但到最后，我们精简了过程，只需半小时。我们利用从这次经验中获得的见解开发了fuzz-utils，一个将断言失败自动转换为单元测试的工具。尽管尚未经过广泛测试，但它对未来合作的潜力令我们兴奋！

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

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

我们分析了Echidna中的完整重现器跟踪（如前一节提到的，这是在此次合作中添加的Echidna功能），并在不同发送者上测试了假设。我们精心制作并执行了一系列单元测试，每次迭代都更多地揭示了底层机制。是时候放大以识别新断言失败中涉及的函数的共性，导致我们专注于processExpiredLock函数。通过仔细审查这个函数，我们发现缺少一个重要的断言：确保在调用带有“重新锁定”选项的函数后，用户锁的数量保持不变。

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

这个发现特别引人注目的是它能够通过各种安全审查和测试逃避检测。结果发现，单元测试正在检查一个不正确的后条件，在其检查中隐藏了错误，在测试套件中掩盖了其错误。这个代码库上的无状态模糊测试（由Curvance在此次合作前构建）实际上在这个错误修复后开始失败。这突出了不仅需要复杂和细致的测试来验证代码库的每个方面，而且需要不断质疑和验证目标代码及其测试的每个方面的必要性。

下一步是什么？

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

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