What does it mean for the data of a virtual machine to be confidential Answering takes us on a journey through low-level systems and high-level mathematics. At re:Invent 2025, Graviton5 was introduced with the AWS Nitro Isolation Engine, a new software component enforcing isolation between virtual machines that was designed from the beginning with formal verification as a first-class consideration. You will learn about the hardware and software that isolate guest virtual machines, our mathematical definition of confidentiality, and the proofs used to establish this property for the Nitro Isolation Engine. No background in virtualization or formal methods is assumed.
CMP501All levelsChalk talkCompute