Confidential computing is a key technology for isolating high-assurance applications from the large amounts of untrusted code typical in modern systems. Existing confidential computing systems cannot be certified for use in critical applications, like systems controlling critical infrastructure, hardware security modules, or aircraft, as they lack formal verification. This paper presents an approach to formally modeling and proving a security monitor. It introduces a canonical architecture for virtual machine (VM)-based confidential computing systems. It abstracts processor-specific components and identifies a minimal set of hardware primitives required by a trusted security monitor to enforce security guarantees. We demonstrate our methodology and proposed approach with an example from our Rust implementation of the security monitor for RISC-V.

翻译：机密计算是一项关键技术，用于将高可信应用程序与现代系统中大量不可信代码隔离开来。现有机密计算系统因缺乏形式化验证，无法获得关键应用（如关键基础设施控制系统、硬件安全模块或飞机系统）的认证。本文提出了一种对安全监视器进行形式化建模与证明的方法。我们引入了一种基于虚拟机（VM）的机密计算系统的规范架构，抽象出处理器特定组件，并确定了可信安全监视器执行安全保证所需的最少硬件原语集合。最后，通过基于RISC-V指令集架构的Rust语言实现的安全监视器实例，展示了我们的方法体系与所提方案。