💻 computer science

Formal Verification of Secure Encrypted Virtualization

本文提出了一个形式化框架，通过对 AMD Secure Encrypted Virtualization (SEV) 的安全保证进行抽象与验证，以严格确保可信执行环境的机密性、完整性和可用性。

原作者： Hansika Weerasena, Amitabh Das, Prabhat Mishra

发布于 2026-06-02

📖 1 分钟阅读☕ 轻松阅读

原作者： Hansika Weerasena, Amitabh Das, Prabhat Mishra

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一座宏伟而繁忙的摩天大楼（云端），里面租用了数百个不同的公司（租户）作为办公室。在普通的建筑中，大楼管理员（Hypervisor）拥有一把万能钥匙，可以打开任何门，窥视任何保险箱，并阅读任何办公桌上的文件。如果管理员是诚实的，那么大家都很安全。但如果管理员变成了间谍，或者被黑客攻击了呢？突然间，每一家公司的秘密都面临风险。

为了解决这个问题，公司开始在建筑内部建造安全房间。这些被称为可信执行环境（TEEs）。具体来说，这篇论文关注的是一种高科技版本的安全房间，叫做 AMD SEV（安全加密虚拟化）。

以下是研究人员的工作内容，用通俗易懂的方式进行解释：

1. 问题所在：“信任我”还不够

AMD SEV 技术就像是一个超级安全的办公室，墙壁由隐形且不可破坏的玻璃制成。即使是大楼管理员（Hypervisor）也无法看到内部或触摸任何东西。计算机硬件本身会对数据进行加密，因此即使有人试图窃取硬盘，得到的也只是一堆乱码。

然而，建造这些房间的人编写了一本手册（规范）来解释它们是如何工作的。但手册仅仅是纸上的文字。它并不能证明这个房间确实是安全的。玻璃上可能存在微小的裂缝，或者建筑师忘记提到的秘密通道。在安全领域，“我们认为它是安全的”是不够的；你需要数学证明。

2. 解决方案：“数学蓝图”

论文作者决定不再靠猜测，而是开始进行证明。他们构建了一个形式化验证框架。

你可以把这想象成一位建筑师，他不只是画出一张建筑图纸，而是创建了一个完美的数学模拟系统。然后，他们在该模拟系统上运行“数字压力测试”，以观察它在任何可能的攻击下是否会崩溃。

他们主要通过两种方式实现了这一点：

设计抽象化： 他们将 AMD SEV 复杂、混乱的技术手册转化为一个简洁、简化的数学模型。这就像是将一本 500 页的说明书变成了一张清晰的流程图。
属性检查： 他们编写了一系列“规则”（属性），即房间为了被视为安全必须遵循的规则。然后，他们使用一个名为 Rosette 的计算机程序来检查数学模型是否会违反这些规则。

3. 三大游戏规则 (CIA)

研究人员根据被称为 CIA 的三个主要目标，检查了 AMD SEV 房间的安全性：

机密性 (Confidentiality) —— “守密者”：
- 规则： 任何人，甚至是大楼管理员，都不应该能读取房间内发生的事情。
- 测试： 他们模拟了一个试图窥探内部的间谍。他们检查了间谍是否能看到访客的“私有内存”或“CPU 寄存器”（计算机的大脑）。
- 结果： 他们验证了 14 条不同的规则。数学证明了，只要 AMD 硬件按照设计工作，间谍就无法看到秘密。
完整性 (Integrity) —— “防篡改封条”：
- 规则： 任何人都不应该能偷偷修改房间内的文件，或将其替换为伪造的文件。
- 测试： 他们模拟了一个破坏者试图重写访客的代码，或者欺骗系统认为旧的、存在漏洞的软件版本就是当前版本。
- 结果： 他们验证了 7 条规则。数学表明，系统拥有一个“反向映射表”（类似于严格的安全日志），可以防止任何人交换页面或将时间回滚到不安全的状态。
可用性 (Availability) —— “电源开关”：
- 规则： 房间应该在你需要时正常工作，且大楼管理员可以在需要时关闭它。
- 测试： 他们检查了两件事：
  1. 管理员是否总能重新获得控制权？是的。 数学证明了管理员总能暂停或停止访客。
  2. 访客是否总能在不被剥夺时间的情况下运行？不是。 数学证明了如果管理员心怀恶意，他们可以选择让访客永远无法运行。系统保证了管理员可以停止你，但并不保证管理员会让你运行。这是该技术的已知局限性。

4. 他们测试的“升级版”

论文不仅研究了基础版的 AMD SEV，还测试了两个更新、更强的升级版本：

SEV-ES： 这为计算机的“大脑”（CPU 寄存器）增加了一层保护。以前，当系统暂停时，管理员可以看到计算机正在思考什么。现在，连思维也会被加密。
SEV-SNP： 这为内存页增加了一个“公证员”系统。它确保内存页属于正确的人，并且没有被替换或篡改。

5. 结论

研究人员成功构建了一个 AMD SEV 系统的数字孪生，并让它经历了一场由 23 项不同安全测试组成的严苛考验。

机密性： 通过了所有测试。
完整性： 通过了所有测试。
可用性： 通过了关于管理员控制权的测试，但也正确识别出访客无法强迫管理员让其运行（这是一个设计特性，而非漏洞）。

总结

这篇论文就像是一支法医工程师团队，他们拿走了一个高科技保险箱，建立了一个完美的数学模型，并向世界证明了，根据数学定律，大楼管理员无法打开这个保险箱。他们不仅仅是说“它看起来很安全”，而是说“我们计算了每一种可能的破解方式，并证明了它无法被破解”。

这为云用户提供了更高水平的信心，确保即使云提供商自己的软件遭到黑客攻击，他们的数据也是安全的。

技术摘要：安全加密虚拟化的形式化验证

问题陈述

现代云计算环境在共享的物理基础设施上托管相互间互不信任的租户，这造成了跨租户攻击和基于 hypervisor 攻击的重大风险。虽然可信执行环境（TEE），特别是基于虚拟机（VM）的 TEE（如 AMD Secure Encrypted Virtualization, SEV），通过硬件辅助隔离来保护代码和数据的机密性与完整性，但其架构文档通常缺乏形式化的安全保证。这些设计的复杂性以及潜在的细微实现缺陷，使得进行严谨的形式化验证变得至关重要，以确保即使在恶意 hypervisor 或受损系统软件存在的情况下，客户机虚拟机（Guest VM）在其整个生命周期内都能保持机密性和未被篡改。现有的针对其他 TEE（例如 Intel SGX、ARM TrustZone）的验证工作由于在信任模型、强制机制和系统交互方面的根本性架构差异，无法直接应用于基于虚拟机的 TEE。

方法论

作者提出了一种利用设计级和属性级抽象来建模并验证 AMD SEV 机密虚拟机的形式化验证框架。该方法论流程如下：

抽象策略：
- 基于设计的抽象： 捕获来自 SEV 规范中所有架构定义的行为和状态转换，以形成基准操作模型。
- 基于属性的抽象： 通过仅关注与特定安全属性（机密性、完整性、可用性）相关的组件和行为来简化系统。
形式化建模：
- 使用求解器辅助编程语言 Rosette 对 AMD SEV 架构（包括 SEV-base、SEV-ES 和 SEV-SNP）进行建模。
- 该模型结合了符号变量、断言和求解器辅助函数，用以表示状态数据结构（如 Guest Context Table、ASID Table、Reverse Map Table）以及应用二进制接口（ABI）函数（如 LAUNCH_START、ACTIVATE、DECOMMISSION）。
- 威胁模型假设存在一个特权对手（hypervisor），该对手能够暂停、终止和操纵系统状态，但受限于硬件强制的隔离机制。
属性定义与验证：
- 框架为机密性（防止未经授权观察内存/寄存器）、完整性（防止未经授权修改或重放数据/状态）和可用性（确保主机和客户机的存活性）定义了形式化模型。
- 验证工作使用结合了 Z3 SMT 求解器 的 Rosette 符号执行引擎进行。系统通过探索执行路径来验证约束并检查反例。

核心贡献

本文做出了以下具体贡献：

全面的形式化模型： 一个定义了机密虚拟机安全边界的形式化模型，明确考虑了具备高级攻击向量的对手。
形式化 CIA 定义： 专门针对基于虚拟机的 TEE 定制的机密性、完整性和可用性（CIA）的形式化定义。
AMD SEV 实现： 在 Rosette 中开发了详细的 AMD SEV 架构形式化模型（涵盖 SEV-base、SEV-ES 和 SEV-SNP），包括状态数据结构和生命周期转换。
对比分析： 对 AMD SEV 的安全措施与其他基于虚拟机的 TEE（如 Intel TDX）进行了批判性评估，强调了在信任根、度量（attestation）和密钥管理方面的架构差异。
形式化验证结果： 成功验证了基于 23 项源自 CIA 安全概念的安全属性的 AMD SEV 架构。

实验结果

作者在 Apple M2 CPU 环境（16 GB RAM）上实现了该模型并验证了 23 项属性：

机密性： 验证了 14 项属性（ $CP_1$ – $CP_{14}$ ）。这些属性涵盖了内存加密强制执行、ASID 隔离、寄存器状态加密（SEV-ES）以及页面验证（SEV-SNP）。所有属性均通过验证。
完整性： 验证了 7 项属性（ $IP_1$ – $IP_7$ ）。这些属性确保了有效的生命周期状态转换、原子性、防止回滚攻击以及在迁移期间正确处理密钥。所有属性均通过验证。
可用性： 对 2 项属性（ $AP_1$ $A P_{1}$ – $AP_2$ $A P_{2}$ ）进行了建模。
- $AP_1$ （主机侧存活性）：已验证。 模型确认 hypervisor 始终可以重新获得控制权。
- $AP_2$ （客户机侧存活性）：未验证。 模型确认在当前的 SEV 技术中无法保证客户机侧的存活性（即在面对恶意 hypervisor 时保证进度），因为 hypervisor 保留了调度控制权。

验证指标：

机密性属性：验证时间约为 20.52 秒。
完整性属性：验证时间约为 12.45 秒。
可用性属性：验证时间约为 3.67 秒。

重要性与主张

本文声称提供了一个严谨的基础，用于定义和验证保障执行环境的关键安全属性。通过建立针对基于虚拟机的 TEE 的 CIA 形式化定义并成功验证 AMD SEV 架构，这项工作证明了形式化方法可以有效地应用于复杂的软硬件协同设计系统。

作者断言，其方法提供了最强的保证，证明架构能够正确执行隔离和保护承诺，解决了基于模拟的方法无法覆盖边缘情况的缺陷。该工作强调，虽然 AMD SEV 提供了强大的机密性和完整性保证（已通过模型验证），但它本质上缺乏针对恶意 hypervisor 的客户机侧可用性保证。论文得出结论，该形式化框架为未来研究如何保障虚拟化 TEE 环境铺平了道路，并为验证云服务的安全态势提供了一种可扩展的解决方案。