Nitro Isolation Engine: formally verifying a production hypervisor

Add to your list(s) Download to your calendar using vCal

• Dominic Mulligan (Amazon Web Services)
• Friday 06 February 2026, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Ioannis Markakis.

Cloud computing relies on hypervisors to enforce isolation between co-tenanted virtual machines. Hypervisors are therefore critical security infrastructure, and assurance of their correctness is paramount. Traditional engineering techniques—code review, testing, fuzzing—provide strong assurance but cannot exhaustively verify that isolation holds across all possible execution paths. Formal verification extends and complements these approaches by establishing mathematical guarantees about system behaviour.

This talk presents our experience applying interactive theorem proving to verify a production hypervisor component: the Nitro Isolation Engine. This is a trusted, minimalist computing base written in Rust, enforcing isolation between virtual machines on AWS Graviton5 EC2 instances. Designed for verification from inception, we have specified the intended behaviour of this component and verified correctness in the Isabelle/HOL interactive theorem prover, producing approximately 260,000 lines of machine-checked models and proofs.

Our verification establishes three key classes of property: Functional correctness: The system behaves as specified for all operations including virtual machine creation, memory mapping, and abort handling. Our total verification approach additionally establishes memory-safety, termination, and absence of runtime errors. Confidentiality: A noninterference-style property demonstrates that guest virtual machine state remains hidden from an expansive definition of observer monitoring system actions, formalised as indistinguishability preservation up to permitted declassification flows. Integrity: Guest virtual machine private state is unaffected by operations on distinct virtual machines. The talk will discuss the verification approach, key proof techniques, and challenges in applying formal methods to production systems.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Martin's interesting talks
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list
• yk449

Note that ex-directory lists are not shown.