Developing provably correct Rust code with Verus

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

自动化推理

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

Verus "程序验证器" 如何通过自动检查代码与功能的数学规范，帮助提高软件项目的安全性保障。

作者

Bryan Parno

2026年8月31日

7分钟阅读

分享

• 复制链接

• 邮件

• X

• 领英

• Facebook

• Line

• Reddit

• QZone

• 新浪微博

• 微信

• WhatsApp

分享到微信

x

收听 • 10:11 分钟

关键要点

• Verus 是一个开源的 Rust 自动程序验证器，它通过形式化数学规范机械地检查代码在所有可能输入下的行为，超越传统测试方法，能够发现边界情况。

• 开发者可以直接使用类似 Rust 的语法在源代码中添加前置条件和后置条件，实现快速反馈循环（不到一秒），并允许 AI 代理协助生成证明。

• Verus 能够对 Rust 的 "不安全" 代码块和使用自定义锁机制的并发代码进行数学验证，为性能关键实现（如 AWS 的 Nitro 隔离引擎）重新建立机器验证的安全保证。

• 亚马逊使用 Verus 证明关键基础设施中核心原语的正确性，该工具已被包括证书验证库、数据格式解析器和 Kubernetes 控制器等分布式系统在内的开源项目采用。

这个回答有帮助吗？

许多开源和行业软件项目，包括亚马逊内部的多个项目，都在采用 Rust 编程语言，因为它提供了与 C 语言相似的性能和灵活性，同时其智能类型系统可以自动防止各种错误和安全漏洞。其结果是比平均水平更快且更正确、更安全的代码。

然而，"更正确和更安全" 并不等同于 "真正正确和安全"。例如，在 C 语言中，越界访问数组——即访问超出内存分配范围的数组元素——是一个危险的错误，可能导致无法预见的后果。在 Rust 中，这将导致程序终止，这确实更安全，但一个正确的程序本身就不会进行越界访问。同样，Rust 无法保证你的程序会计算出你期望的结果，或者不会泄露它有权访问的机密。这就是 Verus 发挥作用的地方。

越界访问数组是一个危险的错误，可能导致无法预见的后果。正确的程序不会允许这种情况发生。

Verus 是什么？

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

例如，你的代码可能实现了一个优化的二分查找算法，用于在排序数组中查找特定值。规范可能指出，当代码成功返回索引时，数组中对应的元素应与目标值匹配。验证器会检查该规范是否适用于所有可能的输入数组和目标值。

与传统测试技术可能尝试几种特定数组但可能遗漏边界情况（例如，如果目标值是数组的最后一个元素或根本不存在怎么办？）不同。程序验证的一个关键方面是构建数学证明，以确保代码符合其规范。在像Verus这样的自动化程序验证工具中，工具会自动处理证明构建中许多繁琐的底层步骤，而人类开发者则提供高层次的指导（例如，设置归纳证明或提供循环不变式）。正如我们在下文讨论的那样，如今，即使这些高层次步骤也可以通过AI实现自动化。

在亚马逊，我们很自豪能够成为Rust基金会的创始成员之一，并且我们广泛使用Rust开发项目，例如Firecracker，它为AWS Lambda和AWS Fargate提供支持，我们的无服务器分布式SQL数据库，以及Nitro Isolation Engine，它为Nitro hypervisor（管理Amazon Web Services（AWS）虚拟机分配的软件）强制执行虚拟机隔离。亚马逊对Rust的热情，加上十多年在自动化推理方面的研究，使我们自然地采用Verus来为我们编写的Rust代码提供更强大的保证。事实上，我们已经使用Verus证明了Nitro Isolation Engine所使用的关键原语的正确性，以及亚马逊内部使用的一些关键基础设施组件的正确性。我们将在未来的文章中探讨这些用例，但目前，我们想向您详细介绍如何使用Verus验证Rust代码。

使用Verus验证Rust代码

通过Verus，Rust开发者可以直接在Rust源文件中为现有Rust代码添加规范（和证明）。以二分查找为例，考虑以下Verus规范（以Rust注释形式编写）对搜索函数现有Rust实现的描述：

一个搜索函数的Rust实现的Verus规范，以Rust注释形式编写。

前置条件（由“requires”关键字指示）指出了函数执行前必须为真的条件。在这种情况下，由于代码实现了二分查找，我们要求数组已排序。后置条件（由“ensures”关键字指示）指出了函数执行后必须为真的条件。在这种情况下，它说明如果函数返回“Some(index)”，则“index”在数组范围内，并且该索引处的值与我们查找的值匹配。

重要的是，它还告诉我们，如果函数返回“None”，则目标值不在数组中。如果没有这个第二条条款，规范可以被一个总是返回“None”的实现所满足！请注意，普通的Rust编译器会忽略这些Verus注释，因此带有Verus注释的代码可以被验证和未验证的项目使用，包括使用Rust构建工具Cargo的项目。

Verus 还专注于提供快速且强大的自动化功能。为此，它使用多种求解器来处理从程序及其规范中生成的证明义务。实际上，这意味着开发者通常能在不到一秒的时间内获得对其代码和证明的反馈，速度足够支持交互式开发循环（包括在 VS Code 等交互式开发环境中显示“红色波浪线”）。

在项目层面，Verus 可以在某些先前自动化程序验证器验证单个函数所需的时间内，验证包含数千行代码和证明的复杂项目。这种强大的自动化和快速反馈循环显然对人类开发者有帮助，但同样也对 AI 代理开发 Verus 证明有帮助，因为自动化意味着代理需要完成的工作更少，可以更快地迭代其证明。

Rust 的类型系统提供了强大的安全性保证，但有时会阻止开发者编写高性能代码。因此，Rust 还允许开发者编写明确标记的“不安全”代码。这种代码仍需满足 Rust 对安全代码的所有预期，但编译器不再机械地检查这些预期；开发者需要自行确保正确性。然而，通过 Verus，开发者可以对他们的不安全 Rust 代码进行数学证明，重新建立经过机器验证的安全性保证。

同样，Rust 著名地提供了“无畏并发”特性，这意味着类型系统会防止开发者在编写并发代码时出现其他编程语言允许的各种错误——即那些至少部分时间并行执行的程序。Verus 在此基础上进一步扩展，使开发者能够证明其并发代码不仅安全，而且正确。

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

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

Verus 在开源生态系统中的应用

除了在亚马逊的应用外，Verus 还被用于证明多种开源项目的有趣属性。以下是一些示例：

• Vest 接收二进制数据格式的描述，并自动生成 Rust 代码来解析和序列化该格式的数据，包括使用 Verus 证明的正确性和安全性。

• Verdict 为 x.509 公钥密码标准提供了一个可证明正确且安全的证书验证库，支持用户提供的验证策略。

• CapybaraKV 项目验证了持久内存日志的正确性和崩溃安全性，即使系统意外崩溃或断电，也能保持数据的规范状态。

• Atmosphere 微内核是一个用 Rust 开发的微内核（最小操作系统），其正确性通过 Verus 进行了验证。

• Anvil 证明了 Kubernetes（一个用于管理云计算的开源系统）控制器的正确性和“活性”。Anvil 表明，在合理假设下，控制器最终会将系统带入稳定状态。

• CortenMM 内存管理系统包含一种新颖的事务接口和可扩展的锁定协议，其并发代码的正确性通过 Verus 进行了验证。

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

研究领域

• 自动推理

标签

• 形式验证
• 形式方法
• 安全
• Firecracker
• AWS Lambda
• Amazon 弹性计算

关于作者

Bryan Parno 是亚马逊学者，卡内基梅隆大学电气与计算机工程及计算机科学的 Kavčić-Moura 教授，他领导着 Secure Foundations 实验室。他的研究重点是长期、根本性地改进安全系统的构建方式，特别关注形式验证的软件。他在密码可验证计算方面的工作获得了 IEEE 安全与隐私研讨会的最佳论文奖和经受时间考验奖，其关于验证系统的研究获得了六次杰出论文奖。Parno 是 ACM 和 IEEE 的高级会员，2011 年入选福布斯“30 岁以下科学精英”榜单，并于 2010 年获得 ACM 博士论文奖。他从卡内基梅隆大学获得博士学位。