BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Nitro Isolation Engine: formally verifying a production hypervisor
  - Dominic Mulligan (Amazon Web Services)
DTSTART:20260206T140000Z
DTEND:20260206T150000Z
UID:TALK243943@talks.cam.ac.uk
CONTACT:Ioannis Markakis
DESCRIPTION:Cloud computing relies on hypervisors to enforce isolation bet
 ween co-tenanted virtual machines. Hypervisors are therefore critical secu
 rity infrastructure\, and assurance of their correctness is paramount. Tra
 ditional engineering techniques—code review\, testing\, fuzzing—provid
 e strong assurance but cannot exhaustively verify that isolation holds acr
 oss all possible execution paths. Formal verification extends and compleme
 nts these approaches by establishing mathematical guarantees about system 
 behaviour.\n\nThis talk presents our experience applying interactive theor
 em proving to verify a production hypervisor component: the Nitro Isolatio
 n Engine. This is a trusted\, minimalist computing base written in Rust\, 
 enforcing isolation between virtual machines on AWS Graviton5 EC2 instance
 s. Designed for verification from inception\, we have specified the intend
 ed behaviour of this component and verified correctness in the Isabelle/HO
 L interactive theorem prover\, producing approximately 260\,000 lines of m
 achine-checked models and proofs.\n\nOur verification establishes three ke
 y classes of property:\nFunctional correctness: The system behaves as spec
 ified for all operations including virtual machine creation\, memory mappi
 ng\, and abort handling. Our total verification approach additionally esta
 blishes memory-safety\, termination\, and absence of runtime errors.\nConf
 identiality: A noninterference-style property demonstrates that guest virt
 ual machine state remains hidden from an expansive definition of observer 
 monitoring system actions\, formalised as indistinguishability preservatio
 n up to permitted declassification flows.\nIntegrity: Guest virtual machin
 e private state is unaffected by operations on distinct virtual machines.\
 nThe talk will discuss the verification approach\, key proof techniques\, 
 and challenges in applying formal methods to production systems.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR