Gambit：一种用于形式验证的Solidity变异测试工具

当开发者编写测试时，他们常常会考虑他们可能引入的常见逻辑错误或他们可能未处理的边界情况。但是，针对那些他们没有想到可能已引入的错误，例如编程或复杂逻辑错误，该如何处理呢？如何编写测试以预见那些未被预见的漏洞？Mutation testing 是解决这一问题的实用方案。它是一种经过充分研究的技术，旨在改善/评估测试套件，并已在大软件公司得到了广泛应用[1]。该技术通常应用于测试上下文，其关键思想是合成程序的故障版本，并检查现有测试套件是否能够捕捉这些故障程序。如果无法捕捉到，那么开发者需要通过设计新的测试用例来扩展测试套件，以捕捉之前未被发现的问题。变异分析是衡量现有测试套件质量的过程，其标准是它能够“击杀”多少个“变异体”（故障程序）。

在这篇博客中，我们讨论了在自动化验证上下文中应用变异测试的努力。我们为Solidity语言开发了一个开源变异生成器，并将其与Certora Prover集成，该工具用于形式化验证智能合约。Certora Prover配有一种声明性领域特定语言CVL，允许用户将其程序的形式化规约书写为“规则”。然后Prover会自动验证程序在所有可能情况下是否满足该规约，或者生成一个反例以显示违反。此程序可以通过检查可执行字节码在代码部署之前识别关键的安全漏洞（你可以在我们的白皮书中详细了解Certora的核心技术）。但用户如何知道规约是否“足够好”？毕竟，形式化验证中最难的挑战之一是编写规约本身。

Gambit：Solidity的开源变异生成器

作为解决这个挑战的第一步，我们构建了Gambit，一个为Solidity设计的开源变异生成器。它遍历AST (抽象语法树)来识别源代码中潜在的变异位置，并直接对源代码进行变异。Gambit是用Rust实现的。文档详细介绍了如何在不同复杂性的Solidity项目中使用Gambit。Gambit生成的变异不仅可以用来评估形式化规约，还可以用来评估测试！我们设想的一个示例应用是与像Foundry这样的测试框架集成，在这里变异测试已经成为一个关注点。正如文档所示，Gambit为用户提供了对要变异的合约和函数的细致控制。这有助于减少生成无用变异体的概率。

使用Gambit的变异进行形式化验证

在Gambit的基础上，我们构建了一个工具，使用Certora Prover自动验证生成的变异与原始形式化规约之间的关系。其目标是利用Gambit生成的变异来评估和改进用CVL编写的形式化规约。在本文的其余部分，我们假设原始程序通过了验证。大致来说，规约“击杀”的变异体越多，CVL规约就越“好”（然而，多余且不可区分的变异也使得这一概念在实践中更复杂），在本文中，_覆盖率_是指被击杀的变异体的百分比。对于每一个变异体，验证有两种主要结果：要么该变异通过验证，要么失败（还有其他情况，如超时，我们将在这里不赘述）。

当一个变异通过验证时，它通常能够提供有关如何改进规约的见解，识别潜在的不完整性或不准确性。对规约的改进可能有不同的方向：有时可能需要新的正确性属性，而在其他情况下，现有的属性可能需要被加强。

当然，也有可能该变异是良性的，例如，它与原始程序语义等价，或只对与验证无关的代码部分进行了变异。

当验证失败且变异被击杀时，它提供了额外的证据，证明规约是“好”的，并能够捕捉到变异引入的错误。它还可以提供有关覆盖率的见解，这些见解通常难以发现！例如，过度近似是一种常用于扩展形式化验证的技巧。变异测试可以揭示规约实际上具有比工程师预期更高的覆盖率——它可能抓住了工程师认为无法捕捉的变异，这进一步增强了对规约质量的信心。

可视化结果

Certora生成了一份可解释且用户友好的报告，以总结验证所有变异体的结果。用户界面是我们与Evil Martians的合作伙伴共同开发的，并且是开源的。任何生成符合用户界面文档格式的报告的测试/验证工具，都可以利用此基础设施可视化变异测试的结果。图1是为Borda合约生成的可视化示例。该示例的完整可视化可以在这里找到。

图1. 验证变异体结果的可视化

图2. 高亮显示规约和变异体

灰点表示变异体，绿色圆圈表示CVL中的规约。绿色圆圈内部的灰点表示与该绿色圆圈相对应的规约捕捉到了该变异体。覆盖率表示通过验证被击杀的变异体的数量。选择一个CVL规约会显示其捕捉到的变异体，选择一个变异体则会显示捕捉该变异体的规约（通过图2中的蓝色高亮显示）。图3展示了用户如何查看与原始程序的差异。

图3. 一个变异体的差异图

在可视化中有两个变异体列表：被捕捉的和未被捕捉的。未被捕捉的变异体可以作为改进规约的指南。可视化结果还显示了实际捕捉到变异体的规约规则的比例。“独立规则”指标报告了一个_变异体_是被单个 CVL规约规则捕捉的被击杀变异体的比例。该指标是测量规约质量的代理；越高越好。如果一个变异体被多个规约捕捉，则表示这些规约在捕捉行为上有重叠，而如果一个变异体只被一个规约捕捉，则表明该规则强且独特，与其他规则没有重叠。

我们正在积极开发额外功能，如更好的等价检测和变异生成。我们希望通过这个工具，用户对他们的规约和整个形式化验证的结果有更多的信心。

在GitHub上查看Gambit

阅读Gambit文档

[1] G. Petrović, M. Ivanković, G. Fraser 和 R. Just, “大规模的实用变异测试：来自谷歌的视角，”发表于 IEEE Transactions on Software Engineering，卷48，第10期，第3900-3912页，2022年10月1日， doi: 10.1109/TSE.2021.3107634。

感谢Certora和Evil Martians的团队对这些贡献！

• 原文链接： certora.com/blog/gambit...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～