使用 Verus 开发可证明正确的 Rust 代码

许多开源和工业软件项目（包括 若干项目 以及 亚马逊的若干项目）正纷纷采用 Rust 编程语言，因为它兼具 C 语言的性能与灵活性，其精巧的类型系统还能自动防止各类缺陷和安全漏洞。结果就是，运行速度快且正确性和安全性高于平均水平。 然而，"更正确、更安全"并不等同于"真正正确、真正安全"。例如，在 C 语言中，数组越界访问——即索引超出分配的内存边界——是一种危险的操作，后果难以预料。在 Rust 中，这种情况会直接终止程序，这固然更安全，但正确的程序本就不该执行越界访问。同理，Rust 无法保证你的程序会计算出你期望的结果，或者不会泄露它有权限访问的机密。这正是 Verus 发挥作用的地方。

什么是 Verus？

Verus 是一款面向 Rust 的开源自动化程序验证器。"程序验证器"会接收关于代码应如何运行的形式化数学规格，并机械地检查代码在所有可能输入下是否符合该规格。

举个例子，你的代码可能实现了一个优化的二分查找算法，用于在有序数组中查找特定值。规格可能规定：当代码成功返回一个索引时，数组中对应位置上的元素必须与目标值匹配。验证器会检查该规格是否对所有可能的输入数组和目标值都成立。

相比之下，传统的测试方法可能只尝试几个特定数组，容易漏掉边界情况（比如目标值恰好在数组最后一个元素，或者根本不存在）。程序验证的核心在于构建数学证明，证明代码符合其规格说明。在 Verus 这样的自动化程序验证器中，繁琐的底层证明步骤由工具自动完成，开发者只需提供高层指导（比如构造归纳证明或给出循环不变量）。如下文所述，如今即使是这些高层步骤，也常常可以借助 AI 自动完成。 Amazon 是 Rust 基金会的创始成员之一，我们对此深感自豪。我们在许多项目中大量使用 Rust，例如支撑 AWS Lambda 和 AWS Fargate 的 Firecracker、我们的无服务器分布式 SQL 数据库，以及 Nitro Isolation Engine——它为 Nitro hypervisor 提供虚拟机隔离保障，而 Nitro hypervisor 是管理 Amazon Web Services (AWS) 虚拟机分配的软件。出于对 Rust 的热情，加上在自动推理领域超过十年的积累，我们很自然地选择用 Verus 为编写的 Rust 代码提供更强的保障。事实上，我们已经用 Verus 证明了 Nitro Isolation Engine 所用关键原语的正确性，也验证了 Amazon 内部多套关键基础设施。这些实际案例会在后续文章中介绍，本文先带你了解用 Verus 验证 Rust 代码到底意味着什么。

用 Verus 验证 Rust 代码

借助 Verus，Rust 开发者可以直接在 Rust 源文件中为现有代码添加规格说明（和证明）。继续以二分查找为例，下面是为 search 函数的现有 Rust 实现添加的 Verus 规格说明（以 Rust 注解形式书写）：

前置条件（由“requires”关键字标记）描述了函数执行前必须成立的约束。在这个例子中，由于代码实现的是二分查找，我们要求数组必须已排序。后置条件（由“ensures”关键字标记）描述了函数执行后必须成立的约束。具体来说，它表明：若函数返回“Some(index)”，则“index”必须在数组的合法范围内，且该索引处的值等于目标值。

关键在于，它还指出：若函数返回“None”，则目标值不存在于数组中。若缺少这条子句，该规范甚至能被一个“永远返回 None”的实现所满足！需要注意的是，常规的 Rust 编译器会忽略这些 Verus 注解，因此带 Verus 注解的代码既可用于已验证的项目，也可用于未验证的项目，包括那些使用 Rust 构建工具 Cargo 的项目。

这个例子还体现了 Verus 的一个核心设计决策，这也是它区别于其他许多 Rust 验证方法的地方。使用 Verus 时，开发者直接在源代码中编写规范与证明，语法风格贴近 Rust。当证明失败时，他们会看到源自代码层面的 Rust 风格错误信息。这种方式让证明始终与实际代码保持同步，也省去了开发者学习一门全新语言和工具的麻烦。它还允许编写代码的人（通常对代码最熟悉）直接参与到正确性证明的过程中。

Verus 还注重提供快速而强大的自动化能力。为此，它使用多种求解器来处理由程序及其规范生成的证明义务。在实际使用中，开发者通常能在不到一秒内获得关于代码和证明的反馈，速度足以支撑交互式开发循环（例如在 VS Code 等交互式开发环境中显示“红色波浪线”提示）。

在项目层面，Verus 能够验证包含数千行代码和证明的复杂项目，其耗时不过于某些传统自动程序验证器验证单个函数所需的时间。这种强大的自动化能力和快速的反馈循环显然有助于人类开发者，同时也帮助 AI 代理生成 Verus 证明——因为自动化减少了代理需要处理的工作量，使其能够更快地迭代证明过程。

Rust 的类型系统提供了强大的安全性保证，但有时它会阻止开发者编写高性能代码。因此，Rust 允许开发者编写明确标记为 "unsafe" 的代码。这类代码仍需遵守 Rust 对安全代码的所有要求，但编译器不再机械地检查这些要求；正确性取决于开发者。借助 Verus，开发者可以数学化地证明其 unsafe Rust 代码的安全性，从而重新建立机器可验证的安全保证。

类似地，Rust 以其"无畏并发"而闻名，即类型系统能防止其他编程语言在编写并发代码时允许的各种错误——换言之，是那些至少部分时间并行执行的程序。Verus 在此基础上构建，使开发者能够证明其并发代码不仅安全，而且是正确的。

例如，并发执行通常涉及锁，锁授予处理器线程对其当前正在操作的数据项的独占访问权。Verus 允许开发者为锁添加不变量属性，这意味着任何获取锁的人都会获得一个满足该不变量属性的值（例如，该值始终为偶数），而在释放锁时，必须证明锁后的值仍然满足该属性。此外，Verus 还支持证明锁实现本身的正确性。这对于 Nitro 隔离引擎等程序尤为重要，它们依赖复杂的自定义锁定方案来实现高性能。

与所有程序验证器一样，Verus 的保证依赖于 Verus 本身的正确性、程序预期行为的"顶层"规范、关于底层运行时（例如 Rust 标准库）的"底层"假设，以及将源代码转换为可执行程序的编译器工具链。我们将在未来的文章中更详细地介绍我们如何增强对这些组件的信心。

开源生态中的 Verus

除了在 Amazon 内部使用，Verus 还被用于为众多开源项目证明一些很有意思的性质。以下是一些例子：

• Vest 接收二进制数据格式的描述，自动生成用于解析和序列化该格式数据的 Rust 代码，并附带 Verus 编写的正确性与安全性证明。
• Verdict 为 x.509 公钥加密标准提供了一个经过正确性和安全性验证的证书校验库，并支持用户自定义校验策略。
• CapybaraKV 项目验证了持久内存日志的正确性和崩溃安全性，即使系统意外崩溃或断电，日志中的数据也能保持格式完好。
• Atmosphere 微内核是一个用 Rust 编写的微内核（极简操作系统），并使用 Verus 完成了正确性验证。
• Anvil 证明了 Kubernetes（一个开源的云计算管理系统）控制器的正确性和“活性”。Anvil 表明，在合理的假设下，控制器最终会将系统带入稳定状态。
• CortenMM 内存管理系统引入了一种带可扩展锁协议的事务接口，其并发代码的正确性已通过 Verus 验证。

Verus 本身是一个免费的开源项目，由学术界和工业界的研究者分布式协作开发。