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

Abstract

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, because they lack formal verification.

Topics & Concepts