Confidential computing is becoming a key technology for isolating high-assurance applications from large amounts of untrusted code typical in modern systems. However, existing confidential computing technologies cannot secure the most critical applications, like systems controlling critical infrastructure, hardware security modules, or aircraft, because they lack formal verification needed for their certification. This paper tackles the above problem by introducing 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. This paper makes a step towards formally modeling and proving the correctness of the security monitor. We present our methodology and demonstrate the proposed approach based on an example from our model and Rust implementation of the security monitor for RISC-V.

翻译：机密计算正成为在隔离高保证应用与当代系统中大量不可信代码的关键技术。然而，现有机密计算技术无法保护最关键的应用程序，例如控制关键基础设施的系统、硬件安全模块或飞行器，因为它们缺乏认证所需的正式验证。本文通过引入一种基于虚拟机（VM）的机密计算系统的通用架构来解决上述问题。该架构抽象了处理器特定组件，并识别了可信安全监控器执行安全保证所需的最小硬件原语集。本文向形式化建模和证明安全监控器正确性迈出了一步。我们展示了方法论，并基于RISC-V架构的安全监控器模型及Rust实现中的示例演示了所提出的方法。