Search Results

Documents authored by Mulligan, Dominic P.

Document
Invited Talk
DOI: 10.4230/LIPIcs.ITP.2026.1
Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk)

Authors: Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, and Konrad Slind

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
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.
Cite as

Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, and Konrad Slind. Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:LIPIcs.ITP.2026.1,
  author =	{Becker, Hanno and Chong, Nathan and Dockins, Robert and Grundy, Jim and Hu, Jason and Mulder, Ike and Mulligan, Dominic P. and Mure, Paul and Parno, Bryan and Paulson, Lawrence C. and Slind, Konrad},
  title =	{{Nitro Isolation Engine: Formally Verifying a Production Hypervisor}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.1},
  URN =		{urn:nbn:de:0030-drops-269757},
  doi =		{10.4230/LIPIcs.ITP.2026.1},
  annote =	{Keywords: Isabelle/HOL, Rust, verification, separation logic, hypervisors}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.1
All Watched Over by Machines of Loving Grace

Authors: Dominic P. Mulligan

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
Modern operating systems are typically built around a trusted system component called the kernel which amongst other things is charged with enforcing system-wide security policies. Crucially, this component must be kept isolated from untrusted software at all times, which is facilitated by exploiting machine-oriented notions of separation: private memories, privilege levels, and similar. Modern proof-assistants are typically built around a trusted system component called the kernel which is charged with enforcing system-wide soundness. Crucially, this component must be kept isolated from untrusted automation at all times, which is facilitated by exploiting programming-language notions of separation: module-private data structures, type-abstraction, and similar. Whilst markedly different in purpose, in some essential ways operating system and proof-assistant kernels are tasked with the same job, namely enforcing system-wide invariants in the face of unbridled interaction with untrusted code. Yet the mechanisms through which the two types of kernel protect themselves are significantly different. In this paper, we introduce Supervisionary, the kernel of a programmable proof-checking system for Gordon’s HOL, organised in a manner more reminiscent of an operating system than a typical LCF-style proof-checker. Supervisionary’s kernel executes at a relative level of privilege compared to untrusted automation, with trusted and untrusted system components communicating across a limited system call boundary. Kernel objects, managed on behalf of user-space by Supervisionary, are referenced by handles and are passed back-and-forth by system calls. Unusually, Supervisionary has no "metalanguage" in the LCF sense, as the language used to implement the kernel, and the language used to implement automation, need not be the same. Any programming language can be used to implement automation for Supervisionary, providing the resulting binary respects the kernel calling convention and binary interface, with no risk to system soundness. Lastly, Supervisionary allows arbitrary programming languages to be endowed with facilities for proof-checking. Indeed, the handles that Supervisionary uses to denote kernel objects may be thought of as an extremely expressive form of capability - in the computer security sense of that word - and can potentially be used to enforce fine-grained correctness and security properties of programs at runtime.
Cite as

Dominic P. Mulligan. All Watched Over by Machines of Loving Grace. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mulligan:LIPIcs.TYPES.2022.1,
  author =	{Mulligan, Dominic P.},
  title =	{{All Watched Over by Machines of Loving Grace}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{1:1--1:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.1},
  URN =		{urn:nbn:de:0030-drops-184449},
  doi =		{10.4230/LIPIcs.TYPES.2022.1},
  annote =	{Keywords: Proof assistant design, operating systems, HOL, LCF, Supervisionary, system description, capabilities}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact