Gambit：用于形式验证的Solidity突变测试工具

Author: Chandrakana Nandi

Editors: Sameer Arora, Thomas Adams

当开发者编写测试时，他们经常考虑可能引入的常见逻辑错误或未能处理的边界情况。但是对于他们没有考虑到的错误，例如编程错误或复杂的逻辑错误，该如何处理呢？如何编写测试以预测未预见的漏洞？突变测试是解决此问题的实用方案。这是一种针对测试套件进行改进/评估的经过充分研究的技术，并已在大型软件公司中得到了广泛的采纳 [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 的合作伙伴开发，并且是 开源的。任何生成报告的测试/验证工具都可以根据 UI 文档 使用此基础设施来可视化突变测试的结果。图 1 是为 Borda 合约 生成的可视化示例。此示例的完整可视化可以在 此处 找到。

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

图 2. 突变和规则的高亮

灰点表示突变，绿色圆圈表示 CVL 中的规范规则。位于绿色圆圈内部的灰点表示与该绿色圆圈对应的规则捕捉了突变。覆盖率表示被验证消灭的总突变数量。选择一条 CVL 规则显示它捕捉的突变，而选择一个突变显示捕捉该突变的规则（图 2 中用蓝色高亮显示）。图 3 显示用户可以查看与原始程序的突变差异。

图 3. 突变的差异

可视化中有两类突变列表：被捕捉的和未被捕捉的。未被捕捉的突变可以用作改善规范的指南。可视化还显示了实际捕捉到突变的规范规则的比例。“单一规则”指标报告的是被单个 CVL 规范规则捕捉到的突变在所有已消灭突变中所占的比例。该指标是衡量规则质量的代理；越高越好。如果多个规则捕捉到一个突变，则表示捕捉到规则之间的行为重叠，而如果一个突变仅被单个规则捕捉，则表示该规则是强、独特的，与其他规则没有重叠。

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

在 GitHub 上查看 Gambit

阅读 Gambit 文档

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

致谢。感谢 Certora 和 Evil Martians 团队的惊人贡献！

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