2026-08-25T02:54:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26975 2026-07-16T09:49:33Z ddc:004 open_access

Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk) Becker, Hanno Chong, Nathan Dockins, Robert Grundy, Jim Hu, Jason Mulder, Ike Mulligan, Dominic P. Mure, Paul Parno, Bryan Paulson, Lawrence C. Slind, Konrad Isabelle/HOL Rust verification separation logic hypervisors 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 330,000 lines of machine-checked models and proofs, and establishing three key classes of property: 1) 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. 2) 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. 3) Integrity: Guest virtual machine private state is unaffected by operations on distinct virtual machines. Currently, our proof coverage extends to verification of the core virtual machine-management hypercalls, guest power management, various utility hypercalls, and a subset of data, instruction, and asynchronous abort handling, and will continue to expand to cover more functionality including PCI device management and virtual GIC (Generic Interrupt Controller) handling. The talk will discuss the verification approach, key proof techniques, and challenges in applying formal methods to production systems. Note that this work builds on decades of academic research across interactive theorem proving, formal specification, separation logic and its automation, and programming language semantics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Hanno Becker and Nathan Chong and Robert Dockins and Jim Grundy and Jason Hu and Ike Mulder and Dominic P. Mulligan and Paul Mure and Bryan Parno and Lawrence C. Paulson and Konrad Slind 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.1 urn:nbn:de:0030-drops-269757 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.1 eng https://creativecommons.org/licenses/by/4.0/legalcode