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

# 形式验证如何让 AWS Nitro 成为首个经过形式验证的云虚拟机监控器 - Amazon Science 来源：https://www.amazon.science/blog/ec2s-formally-verified-isolation-engine-provides-mathematical-assurance-of-virtual-machine-isolation 今天，我们宣布了 Amazon Web Services (AWS) Elastic Compute Cloud (EC2) 全新 M9g 和 M9gd 实例的正式可用性，这是首批搭载 Graviton5（我们最新一代通用 CPU）的实例类型。Graviton5 将核心数量从上一代的 96 核翻倍至 192 核。 它们也是首批使用全新 Nitro 隔离引擎的实例类型。Nitro 隔离引擎是 Nitro 虚拟机监控器的一个组件，其唯一职责是隔离虚拟机 (VM)。在这篇文章中，我们将解释如何使用 Isabelle/HOL（高阶逻辑）证明助手——一种机械地检查推理步骤是否符合逻辑规律的软件——来证明 Nitro 隔离引擎行为正确，并能强制虚拟机之间的隔离。Nitro 隔离引擎是首个部署在商业云环境中并经过形式验证的虚拟机监控器的关键组件。 我们的 Isabelle/HOL 模型和证明包含 330,000 行经过机器检查的数学内容。其规模与 seL4 相当，后者是一个里程碑式的项目，首次证明了现实操作系统验证的可行性，并启发了我们的工作。然而，与 seL4 不同，Nitro 隔离引擎专为商业云环境设计，并作为 Graviton5 用户的常开功能在生产硬件上发布。 我们在亚马逊 2025 re:Invent 大会上的演讲 介绍了我们的形式验证方法论。这篇博客将非正式地概述我们形式验证工作的主要方面以及它们如何协同工作。 ## 什么是分离内核？ John Rushby 于 1981 年创造了“分离内核”一词，用来描述一个最小的操作系统组件，它将系统划分为隔离的 compartment。关键思想：将策略与机制分离。分离内核不决定隔离什么、如何分配资源或调度哪些虚拟机：这些决策由其他地方作出。相反，它只专注于强制执行隔离，这种明确的目标使分离内核比完整的操作系统内核简单得多。 自 2017 年推出以来，Nitro 虚拟机监控器一直负责在 EC2 中强制执行隔离，但它也处理业务逻辑、设备驱动程序和 AWS 特定功能。这种复杂性使得证明正确性更加困难。此外，Nitro 虚拟机监控器最初并非为验证而设计。 将虚拟机监控器的关键隔离逻辑提炼成一个最小组件——Nitro 隔离引擎——使其足够小以便于验证和审计，为客户提供前所未有的可见性，了解隔离是如何实施的。我们还用 Rust 语言编写了 Nitro 隔离引擎，这种语言更自然地适合形式验证。 Nitro 虚拟机监控器仍然处理策略——VM 创建、资源分配、迁移、调度——但它现在被降权，必须请求 Nitro 隔离引擎来执行任何涉及客户状态的操作。Nitro 隔离引擎在执行前检查每个请求。 启用 Nitro 隔离引擎的服务器的系统架构。 ## 规范与证明 我们工作的两个关键部分是规范和证明。形式规范精确地捕获了系统的预期行为，而证明则确立了实现满足这些规范。 我们关于 Nitro 隔离引擎的定理涉及四种类型的属性： 1. **机密性和完整性**。只允许经过授权的信息流。例如，客户内存分配在重用之前总是被擦除。 2. **功能正确性**。实现的行为与规范完全一致。 3. **无运行时错误**。没有诸如 Rust 中 unwrap None 选项值之类的运行时错误——这是一种会导致程序停止执行的错误命令调用。 4. **内存安全**。没有诸如缓冲区溢出和空指针解引用之类的问题。 在实践中，我们共同处理后三个属性，作为功能验证结果，而机密性和完整性则单独处理，因为我们对每个属性使用不同的证明技术。 ## 功能验证 对于功能验证，关键部分包括：Rust 语言核心子集的形式化，称为 μRust（“微 Rust”）；使用分离逻辑表达精确规范的表述性规范语言；以及一种验证技术——最弱前置条件演算——配合自定义证明自动化，用于证明程序相对于其规范的正确性。这些都是我们在 2025 年作为 AutoCorrode 库开源的通用证明基础设施的一部分。 更详细地说，μRust 是 Rust 编程语言的一个受限子集，它足够表达性强，可以编写 Nitro 隔离引擎，但又适合形式推理，因为我们有意排除了高级 Rust 特性，比如 trait 和动态分发。μRust 的形式语义被定义为 Isabelle/HOL 中的浅层嵌入，这意味着 μRust 的含义是用高阶逻辑（Isabelle/HOL 的“宿主语言”）来定义的。 μRust 程序的规范被定义为一个带有前置条件和后置条件的合约，这些条件是关于执行程序前后系统状态的断言。我们的规范指定了“完全正确性”，这意味着在所有满足前置条件的状态下，程序总是终止，并且结果状态满足后置条件。这种完全正确性条件也意味着程序是内存安全的，并且没有运行时错误。我们的规范使用分离逻辑编写，这是一种专为推理低级指针操作程序而设计的逻辑。 尽管分离内核相对简单，但在验证 Nitro 隔离引擎时，我们仍然处于形式验证可能性的边缘，我们的规范和证明都变得非常庞大。例如，以下规范捕获了当正在执行的客户虚拟 CPU 试图打开自身（一个错误请求）时会发生什么： PSCI_CPU_ON 的规范，这是一种用于打开目标 CPU 的电源状态函数。 虽然上面的规范很复杂，但它捕获的内容直观上很简单：在这种情况下，Nitro 隔离引擎发现，作为调用者，虚拟 CPU 必须已经打开，因此它返回一个定义的错误代码 *AlreadyOn*。系统状态的其他所有内容保持不变。规范的复杂性反映了我们模型设计的深度，以及为了到达 Nitro 隔离引擎实现中的这一点，已经必须执行的其他几个错误检查。 为了证明 μRust 程序相对于其规范的正确性，我们使用标准的最弱前置条件演算。最弱前置条件演算是一种系统的方法，用于识别确保程序在特定操作后的状态不超出某些指定状态范围的最小限制性约束。例如，表达式 "*x + y*" 的最弱前置条件是 x 和 y 的值不能导致加法溢出的状态。然后证明义务是表明合约的前置条件蕴含计算出的最弱前置条件。 ## 机密性和完整性 对于机密性和完整性，第一个关键部分是一个高级规范，它将 Nitro 隔离引擎的行为捕获为一个转移关系，其中系统的每个“高级”步骤（例如，超级调用）都是一个原子转移。这个规范被严格地关联到我们在功能验证结果中使用的更具体的分离逻辑规范，这使用了另一个称为精化的证明理念。第二个关键部分是非干扰的思想。 非干扰是我们用来使机密性和完整性在数学上精确的不可区分性保持概念。这个想法是，如果一个步骤之前两个状态对观察者来说不可区分，那么之后它们必须保持不可区分。这捕获机密性的直观原因是，观察者因为这个步骤而没有学到任何新东西。 理解为什么不可区分性保持可以保证机密性是很微妙的。考虑两个简单的机器，A 和 B，每个都有一个公共寄存器和一个私有寄存器。如果它们的公共寄存器匹配，则观察者认为它们不可区分：私有寄存器是隐藏的。在下图中，A 和 B 是不可区分的： 一个机密性违反的例子。 现在考虑如果执行一个程序，该程序根据私有寄存器分支，将 1 赋值给公共寄存器，会发生什么。结果机器 A' 和 B' 现在有不同的公共寄存器——它们是可区分的！一个聪明的观察者可以利用这一点推断出原始的私有值，而这种未能保持不可区分性对应于非法的信息流向观察者。 ## 更多精彩即将呈现 希望你喜欢我们对验证工作主要部分的概述。我们的工作还有许多其他方面，例如一致性测试以及我们如何处理并发代码的推理，我们期待在未来的文章中分享。