Towards a Formally Verified Security Monitor for VM-based Confidential Computing

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.