  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.
