Curvance: 不变性释放 - Trail of Bits博客
欢迎深入了解我们与Curvance共同进行的不变性开发世界。六年来，我们一直在常规代码审查评估中构建不变性，但与Curvance的合作标志着我们首个正式的不变性开发项目，其中我们专注于开发和测试不变性。
在九周的合作中，我们编写并测试了216个不变性，帮助我们发现了13个关键发现。我们还找到了显著增强工具的机会，包括高级跟踪打印和语料库保存。这个项目是 navigating 学习曲线和完成技术壮举的旅程，本文将重点介绍我们的协作努力和团队合作在帮助我们应对挑战中的关键作用。是的，我们也会提到在这个项目中经历的脑细胞测试时刻！
创建高质量的模糊测试套件
模糊测试套件的成功基于其不变性的质量。在整个项目中，我们专注于微调每个不变性的准确性和相关性。模糊测试本质上就像有聪明的猴子在键盘上测试不变性，其有效性 heavily 依赖于它们的精确性。我们与Curvance的九周旅程涉及将代码库属性的深入讨论转化为精确的英语解释，然后将它们编码为可执行的测试，如下面的截图所示。
从一开始，Curvance的Chris经常可以帮助澄清代码的预期行为并解释Curvance的设计选择。他的见解总是澄清复杂的功能和行为，并且他总是帮助进行动手调试和检查我们的不变性。这次合作之所以如此富有成效，得益于Chris的持续反馈和全程与我们并肩工作。谢谢Curvance！
我们成功背后的工具（和支持团队）
除了Curvance的参与，我们内部团队 behind Echidna、Medusa和CloudExec的支持帮助我们的项目成功。他们对问题的快速响应，特别是在广泛的重基和复杂调试期间，至关重要。Curvance的合作将这些工具推到了极限，我们为面临的挑战必须想出的解决方案导致了这些工具的重大增强。
CloudExec被证明对于将长时间模糊测试作业部署到DigitalOcean是无价的。我们将其与Echidna和Medusa集成以进行 prolonged 运行，使Curvance能够轻松设置自己未来的模糊测试运行。我们 pinpointed CloudExec的改进领域，如其输出数据的保存，您可以在其GitHub问题跟踪器上看到。我们已经解决了许多这些问题。
Echidna，我们基于属性的以太坊合约模糊测试器，在 falsifying 断言中至关重要。我们首先在探索模式下使用Echidna广泛覆盖Curvance代码库，然后我们进入断言模式，使用 anywhere 从1000万到1000亿次迭代。在我们九周的合作中，Echidna的 intense 使用帮助我们发现了工具的关键改进领域，使其更容易调试和保留 explored 代码区域的状态。
Medusa，我们基于geth的实验性模糊测试器，在 falsifying Curvance上的不变性的覆盖努力中 complement Echidna。在我们能使用Medusa进行这次合作之前，我们需要修复一个已知的内存不足错误。这个错误的修复——以及CloudExec中实施的修复以帮助它更好地保存输出数据—— critically 改进了工具并帮助最大化我们对Curvance代码的覆盖。它开始运行后立即，它在代码中发现了一个中等严重性的错误，Echidna错过了。（Echidna最终在我们更改了块时间延迟后找到了这个错误， likely 由于模糊测试器的非确定性。）
漫长而曲折的道路
虽然我们得到了工具团队和客户的最好支持，但我们在整个项目中仍然面临着相当大的挑战——从需要跟上Curvance的持续开发，到调试断言失败的挑战。但通过 meeting 这些挑战，我们学到了关于不变性开发性质的重要教训，并且我们能够实施对我们工具的关键升级以改进我们的整体过程。
竞速跟上Curvance的代码更改
Curvance代码库的更改——如函数移除、函数参数的添加、参数和错误消息的调整，以及源合约的重命名——经常通过使现有不变性无效或导致一系列断言失败来挑战我们的模糊测试套件。最终，这些更改使我们的现有语料库项过时和不可用，我们必须 constantly 重基我们的模糊测试套件并修订现有和新的不变性，以确保它们继续与 evolving 系统相关。这个迭代过程 paralleled 客户的代码开发，呈现了真阳性（客户代码中的实际错误）和假阳性（由于不正确或过时的不变性导致的失败）的混合。这样的结果 emphasized 模糊测试不是静态的、一次性的设置；它需要持续的维护和更新，类似于任何活跃代码库的开发。
理解每个重基后不变性更改背后的 rationale 至关重要。没有 fully 掌握其含义的草率调整可能会 inadvertently 掩盖错误， undermining 模糊测试套件的有效性。保持套件活跃和相关与代码库本身的开发一样 vital。这不仅仅是让模糊测试器运行；而是保持其与它测试的系统的 alignment。记住，模糊测试套件的真正力量在于其不变性的准确性。
关键工具升级和经验教训
在提交a96dc9a中Lendtroller合约的名称更改为MarketManager后，我们必须进行 significant 重基。这个更改 drastically 影响了我们的工作，因为Echidna刚刚使用CloudExec在云中完成了43天的运行。这个 nonstop 执行允许Echidna开发一个详细的语料库，能够 autonomously 处理复杂清算。不幸的是，这个更改使这个语料库过时，每个语料库项导致Echidna工作线程在事务重放时崩溃。随着我们15个工作线程的设置，只需要14个更多无法重放的事务，所有Echidna工作线程就会崩溃，完全停止Echidna：
由于Curvance的代码更改，我们的重基导致了一个 significant 问题：我们的模糊测试器无法再访问探索复杂状态所需的MarketManager功能，如发布抵押和借入债务。这个问题 prompt 我们对Echidna进行关键更新， specifically 增强其验证和重放语料库序列而不崩溃的能力。我们还对Medusa进行了更新以改进其跟踪语料库健康和修复启动恐慌的能力。关于维护动态语料库的 extended 讨论 ensued，我们的工程总监介入 manually 调整语料库，提供了一些缓解。
我们 shifted 我们的策略以适应新代码库缺乏覆盖的情况。我们为合约名称更改前的代码库版本开发了特定于清算的不变性，同时以不同模式运行更新版本以提升覆盖。CloudExec的新功能，如命名作业、改进的输出目录检查点和失败作业的检查点，在区分和管理这些运行中是关键的。尽管有所有这些改进，我们 let go 了旧语料库并选择将设置功能集成到关键合约中以加速覆盖。虽然在增加覆盖方面有效，但这个策略引入了偏见，特别是在清算场景中，通过依赖静态值。这个限制，在代码库中用/// @coverage:limitation标签标记， underscores 在我们的有状态测试中拓宽输入范围以确保全面系统探索的重要性。
试验和磨难：调试
Curvance不变性开发报告主要 highlight 了我们调试的结果，而没有深入探讨这些发现背后的复杂调查和根本原因分析 journey。这个过程的一部分，涉及一旦断言失败被识别后的详细分析，需要 significant 努力。
我们的主要挑战是剖析长调用序列， often 范围从9到70个事务，这需要 deep scrutiny 以识别错误和意外值 crept in 的地方。一些序列 spanned 高达2900万个块或包括超过6年的时间延迟，为我们的系统行为理解添加了 layers 的复杂性。为了解决这个问题，我们必须 manually 插入日志以获取详细的状态信息，将调试变成 exhaustive 和 manual endeavor：
我们 manually 缩小事务序列的能力 hinged 于我们对Curvance系统的 deep 理解。这个 detailed 知识对于我们有效识别哪些事务对于 uncovering 漏洞 essential 以及哪些可以丢弃至关重要。随着我们在整个项目中获得这个 deeper 洞察，我们 streamline 事务序列的能力 markedly 改进。
基于我们梳理事务序列的工作，我们在Echidna中实施了一个丰富的重现器跟踪功能，提供我们执行期间系统的详细跟踪和事务失败序列每一步系统状态的 elaborate 打印输出。同时，我们还向Medusa添加了事务序列的缩小限制以修复间歇性断言失败，并且我们更新了Medusa的覆盖报告以增加其可读性。这些更新后Echidna跟踪打印的 stark 差异可以 easily 在下面的图中看到：
最后，我们基于我们合作期间的大多数断言失败创建了相应的单元测试。最初，将失败转换为单元测试是 manual 和 time-consuming，但到最后，我们 streamlined 过程只需半小时。我们使用从这个经验中获得的 insights 开发了fuzz-utils，一个将断言失败自动转换为单元测试的工具。虽然它尚未 extensively 测试，但其未来合作的潜力 excites 我们！
一个锁太多：TOB-CURV-4背后的故事
在Curvance代码库的 significant 更改后，我们遇到了一个 puzzling 断言失败。最初，我们怀疑它可能是一个假阳性， major 代码更改的常见发生。然而，在检查Curvance源代码的更改后，根本原因不是 immediately 明显， leading 我们进入一个复杂和彻底的调试过程。
我们分析了Echidna中的完整重现器跟踪（一个在这次合作中添加的Echidna功能，如前一节所述），并且我们在不同发送者上测试了假设。我们 crafted 并执行了一系列单元测试，每次迭代 shedding 更多 light 于 underlying 机制。是时候 zoom out 以识别新断言失败中涉及功能的共性， leading 我们专注于processExpiredLock函数。通过 closely scrutinizing 这个函数，我们发现了一个重要的断言缺失：确保用户锁的数量在调用带有“重新锁定”选项的函数后保持不变。
当我们 reran 模糊测试器时，它 immediately 揭示了错误：这样的调用将处理过期锁但 incorrectly 授予用户一个新锁而不移除旧锁， leading 到总锁数的意外增加。这在combineAllLocks函数中导致了所有形式的问题：合约总是认为用户比实际多一个锁。Eureka！
这个发现 particularly striking 的是其 ability 通过各种安全审查和测试 elude 检测。单元测试，如它 turned out，正在检查一个不正确的后条件， concealing 错误在其检查中， masking 其错误在测试套件内。这个代码库上的无状态模糊测试测试（由Curvance在这次合作前构建）实际上在这个错误修复后开始失败。这 highlighted 不仅需要复杂和 meticulous 测试验证代码库的每个方面，而且需要 continually questioning 和 validating 目标代码的每个方面——及其测试。
下一步是什么？
反思我们与Curvance的旅程，我们认识到全面安全工具包对于智能合约的重要性，包括单元、集成和模糊测试，以 uncover 系统复杂性和潜在问题。我们过去九周的合作允许我们 meticulously 检查和理解系统，增强我们发现的准确性并深化我们的相互知识。与Curvance紧密合作 proven crucial 在揭示技术的 intricacies， leading 到开发一个有状态模糊测试套件，将随着代码 evolve 和 expand，确保持续的安全和 insights。
如果您正在开发一个项目并想探索有状态模糊测试，我们很乐意与您聊天！