EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation

形式验证如何使 AWS Nitro 成为首个经过形式验证的云虚拟机监视器 - 亚马逊科学

自动化推理

EC2 的形式验证“隔离引擎”为虚拟机隔离提供数学保证

将“分离内核”从 Nitro 安全系统其余部分分离，并仅使用 Rust 编程语言的子集进行编码，使其形式验证成为可能。

作者：

Dominic Mulligan

,

Nathan Chong

2026 年 6 月 10 日

7 分钟阅读

分享

• 复制链接

• 邮件

• X

• 领英

• Facebook

• Line

• Reddit

• QZone

• 新浪微博

• 微信

• WhatsApp

分享到微信

x

关键要点

• Nitro 隔离引擎是 Nitro 虚拟机监视器的核心组件，后者是首个部署在商业云环境中的形式验证虚拟机监视器，确保虚拟机之间的正确行为和隔离执行。

• Nitro 隔离引擎的形式验证使用 Isabelle/HOL 证明助手实现，生成了 33 万行机器验证的数学代码，规模与 seL4 项目相当。

• 验证过程包括对 Rust 语言核心子集（μRust）的形式化，使用分离逻辑进行规范，应用最弱前条件演算进行证明，所有内容均包含在开源的 AutoCorrode 库中。

• 验证覆盖了四类属性：保密性与完整性、功能正确性、无运行时错误和内存安全，其中保密性与完整性通过非干扰和不可区分性保持分别处理。

• Nitro 隔离引擎专为商业云环境设计，是 Graviton5 用户的始终启用功能，提供前所未有的隔离执行可见性。

这回答有帮助吗？

今天，我们宣布 Amazon Web Services（AWS）弹性计算云（EC2）的新 M9g 和 M9gd 实例已正式发布，这是首款搭载 Graviton5 的实例类型，Graviton5 是我们最新一代通用 CPU。Graviton5 将核心数量从上一代的 96 个翻倍至 192 个。

它们也是首款使用新 Nitro 隔离引擎的实例类型，该引擎是 Nitro 虚拟机监视器的组件，其唯一职责是隔离虚拟机（VM）。在本文中，我们将解释我们如何使用 Isabelle/HOL（高阶逻辑）证明助手——一种通过机械检查推理步骤以确保符合逻辑规则的软件——来证明 Nitro 隔离引擎的行为正确性并强制虚拟机之间的隔离。Nitro 隔离引擎是首个部署在商业云环境中的形式验证虚拟机监视器的关键组件。

我们的 Isabelle/HOL 模型和证明包含 33 万行机器验证的数学代码。其规模与 seL4 相当，后者是首次证明现实操作系统验证可行的里程碑项目，也是我们工作的灵感来源。然而，与 seL4 不同的是，Nitro 隔离引擎专为商业云环境设计，并作为 Graviton5 用户的始终启用功能部署在生产硬件上。

我们在亚马逊2025年re:Invent大会的演讲中介绍了我们的形式验证方法论，而我们的白皮书则对结果的重要方面（如范围和假设）进行了更深入的探讨。这篇博文将非正式地概述我们形式验证工作的主要方面，以及它们如何相互配合。

什么是隔离内核？

约翰·拉希比（John Rushby）于1981年首次提出“隔离内核”（separation kernel）这一术语，用来描述一种最小化的操作系统组件，它将系统划分为相互隔离的区域。核心思想是将策略与机制分离。隔离内核不决定要隔离什么、如何分配资源或调度哪些虚拟机，这些决策由其他组件完成。相反，它专注于强制执行隔离，这种明确的目标使隔离内核的实现比完整操作系统内核简单得多。

自2017年推出以来，Nitro虚拟机管理程序（Hypervisor）一直负责在EC2中强制执行隔离，但它还处理业务逻辑、设备驱动程序和AWS特定功能。这种复杂性使得证明其正确性变得困难得多。此外，Nitro虚拟机管理程序最初并未设计为可验证。

将虚拟机管理程序的关键隔离逻辑提炼为一个最小组件——Nitro隔离引擎（Nitro Isolation Engine），使其足够小，便于验证和审计，从而为客户提供前所未有的可见性，了解隔离是如何执行的。我们还使用Rust语言编写了Nitro隔离引擎，这种语言更自然地适用于形式验证。

Nitro虚拟机管理程序仍然处理策略——虚拟机创建、资源分配、迁移和调度——但现在它被降权，必须向Nitro隔离引擎请求任何涉及客户机状态的操作。Nitro隔离引擎在执行任何操作之前会检查每个请求。

启用Nitro隔离引擎的服务器系统架构。

规格与证明

我们工作的两个关键部分是规格说明和证明。形式规格说明精确地捕捉系统的预期行为，而证明则确立实现符合这些规格。

我们关于Nitro隔离引擎的定理涉及四种类型的属性：

• 机密性和完整性。只能发生授权的信息流。例如，客户机内存分配在重复使用前总是会被清除。

• 功能正确性。实现的行为与规格说明完全一致。

• 没有运行时错误。不存在诸如Rust中None选项值的unwrap等运行时错误——这会导致程序终止的错误命令调用。

• 内存安全性。没有缓冲区溢出和空指针解引用等问题。

实际上，我们通常将后三个属性作为功能验证结果一起处理，而将机密性和完整性单独处理，因为我们为每个属性使用了不同的证明技术。

功能验证

在功能验证方面，关键部分包括对Rust语言核心子集的形式化（称为μRust（“微Rust”））；使用分离逻辑的表达性规格说明语言，用于精确捕捉规格；以及一种验证技术——最弱前置条件演算（weakest-precondition calculus），并配有自定义的证明自动化工具，用于证明程序相对于其规格的正确性。这些内容都是我们于2025年开源的通用证明基础设施AutoCorrode库的一部分。

更具体地说，μRust 是 Rust 编程语言的一个受限子集，它具有足够的表达能力来编写 Nitro 隔离引擎，同时由于我们有意排除了高级 Rust 特性（如 trait 和动态调度），因此适合形式化推理。μRust 的形式语义在 Isabelle/HOL 中定义为浅层嵌入，这意味着 μRust 的含义是通过高阶逻辑（Isabelle/HOL 的“宿主语言”）来定义的。

μRust 程序的规范被定义为包含前置条件和后置条件的契约，这些条件是对程序执行前后系统状态的断言。我们的契约规定了“完全正确性”，这意味着在所有满足前置条件的状态中，程序始终能终止，并且最终状态满足后置条件。这种完全正确性条件也意味着程序具有内存安全性且没有运行时错误。我们的规范使用分离逻辑（Separation Logic）编写，这是一种专门用于推理低级指针操作程序的逻辑。

尽管分离内核相对简单，但在验证 Nitro 隔离引擎时，我们仍然处于形式化验证能力的极限边缘，我们的规范和证明规模都变得非常庞大。例如，以下规范描述了当运行中的客户虚拟 CPU 尝试自行启动（一个错误请求）时会发生的情况：

PSCI_CPU_ON 功耗状态函数的规范，用于启动目标 CPU。

尽管上述规范较为复杂，但它所描述的情况在直觉上是显而易见的：在这种情况下，Nitro 隔离引擎会发现，要作为调用者，虚拟 CPU 必须已经处于开启状态，因此会返回一个定义好的错误码 AlreadyOn。系统状态的其他所有内容都保持不变。规范中的复杂性反映了我们建模的深度，以及在实现 Nitro 隔离引擎的这一阶段，必须已经完成了其他多个错误检查。

为了证明 μRust 程序相对于其规范的正确性，我们使用标准的最弱前置条件演算（weakest-precondition calculus）。最弱前置条件演算是系统化识别最宽松约束的方法，以确保特定操作后程序状态不会超出某些指定状态范围。例如，表达式 "x + y" 的最弱前置条件是 x 和 y 的值不会导致加法溢出的状态。证明义务则是展示契约的前置条件蕴含计算出的最弱前置条件。

保密性和完整性

在保密性和完整性方面，第一个关键部分是描述 Nitro 隔离引擎行为的高层规范，该规范以状态转移关系的形式定义，系统每个“高层”步骤（例如超调用）都是一个原子转移。该规范与我们在功能验证结果中使用的更具体的分离逻辑规范严格关联，后者使用另一种称为精化（Refinement）的证明思路。第二个关键部分是非干扰（noninterference）的概念。

非干涉是用于使保密性和完整性具有数学精确性的不可区分性保持概念。其核心思想是：如果两个状态在某个步骤之前对观察者来说是不可区分的，那么在该步骤之后它们仍然必须保持不可区分性。这种特性之所以能捕捉保密性，直观原因是观察者在此过程中并未学到任何新信息。

理解为什么不可区分性保持能保证保密性需要深入思考。设想两台简单的机器A和B，每台机器各有一个公共寄存器和一个私有寄存器。当它们的公共寄存器内容一致时，观察者会认为它们是不可区分的——因为私有寄存器是隐藏的。在下图中，A和B是不可区分的：

保密性违规示例。

现在考虑执行一个根据私有寄存器值分支的程序，将1赋值给公共寄存器。执行后得到的机器A'和B'现在具有不同的公共寄存器——它们变得可区分了！精明的观察者可以利用这一特性推断出原始私有值，这种不可区分性未能保持的现象对应着信息向观察者的非法流动。

更多内容即将呈现

希望您喜欢我们验证工作主要组成部分的概述。我们的研究还有许多其他方面，例如符合性测试以及如何处理并发代码的推理方法，这些内容我们很期待在未来的文章中与您分享。

研究领域

• 自动推理
• 云计算与系统
• 安全、隐私与滥用预防

标签

• 形式化验证
• 可证明安全性

关于作者

Dominic Mulligan是亚马逊自动推理团队的首席应用科学家。

Nathan Chong是亚马逊自动推理团队的首席应用科学家。他的研究重点是并发系统代码的正确性，特别是在硬件-软件边界处的验证问题。