使用 Move Prover 对智能合约进行快速可靠的形式化验证⋆
David Dill, Wolfgang Grieskamp()⋆⋆,
Junkil Park, Shaz Qadeer, Meng Xu, and Emma Zhong
Novi Research, Meta Platforms, Menlo Park, USA
摘要。 Move Prover (MVP) 是用 Move 编程语言编写的智能合约的形式化验证器。 MVP 具有表达性强的规范语言，并且足够快速和可靠，可以由开发人员和集成测试定期运行。
除了智能合约和 Move 语言的简单性之外，MVP 的实用性还包括三种实现方法：
- (1) 无别名内存模型，
- (2) 细粒度不变检查，以及
- (3) 单态化。
Diem 区块链的全部 Move 代码已被广泛指定，并且可以在几分钟内被 MVP 完全验证。 在集成到 GitHub 上的开源存储库之前，必须成功验证 Diem 框架中的更改。
关键词：智能合约·形式化验证·Move Language·Diem Blockchain
介绍
Move Prover (MVP) 是一种用于智能合约的形式化验证工具，通常在代码开发过程中使用。验证快速且可预测地完成，使运行 MVP 的体验类似于运行编译器、linter、类型检查器和其他开发工具的体验。
构建快速验证器并非易事，在本文中，我们想分享使这成为可能的最重要的工程和架构决策。使验证更容易的一个因素是将其应用于智能合约。
智能合约比传统软件更容易验证，至少有三个原因：
- 1）它们的代码量很小，
- 2）它们在定义明确的隔离环境中执行，
- 3）它们的计算通常是顺序的、确定性的，并且与环境的交互最少（例如，没有显式的 I/O 操作）。
同时，形式化验证对智能合约的拥护者更具吸引力，因为智能合约如果行为不端可能带来巨大的财务和监管风险，已经发生的巨额损失证明了这一点 [28,18,21]。
MVP 成功的另一个关键因素是与 Move 编程语言 [25] 的紧密耦合。
Move 是作为 Diem 区块链 [23] 的一部分开发的，旨在从一开始就用于形式验证。
Move 目前正在与 MVP 共同发展。该语言支持指定函数的前、后和中止条件，以及数据结构和全局持久内存内容（即区块链的状态）的不变量。
使验证更加困难的一个特征是量化可以在规范中自由使用。
尽管规范丰富，MVP 能够在几分钟内验证 Diem 区块链的完整 Move 实现（称为 Diem 框架 [24]）。
该框架提供了管理账户及其交互的功能，包括多种货币、账户角色和交易规则。它由大约 8,800 行 Move 代码和 6,500 行规范（包括两者的注释）组成，这表明该框架被广泛指定。
更重要的是，验证是完全自动化的，并且通过单元和集成测试连续运行，我们认为这证明了该方法的实用性。
在集成测试中运行证明者需要的不仅仅是速度：它需要可靠性，因为在这种情况下，有时会工作但有时会失败或超时的测试是不可接受的。
MVP 是一个重要且不断发展的软件，它已经在许多方面进行了调整和优化。
因此，要准确定义哪些实施决策会导致快速和可靠的性能并不容易。
然而，自 MVP [31] 的早期原型描述以来，我们至少可以确定三个主要想法，这些想法导致速度和可靠性显着提高：
- 基于 Move 语义的无别名内存模型，类似于 Rust 编程语言；
- 细粒度的不变量检查，确保不变量保持所有状态，除非开发人员明确暂停它们；
- 单态化，它在 Move 的通用结构、函数和规范属性中实例化类型参数。
所有这些改进的综合效果将一个有效的工具转变为一个几乎总是在不到 30 秒内完成的工具。 此外，还有许多其他改进，包括更具表现力的规范语言、减少误报和错误报告。
论文的其余部分首先介绍了 Move 语言以及如何使用 MVP，然后讨论了 MVP 的设计和上面的三个主要优化。 还有一个附录描述了函数规范的注入。