LFCS Seminar: Tuesday 26th May: Dominic Mulligan | LFCS

Tue, 26 May, 4.10pm

Venue: IF G.03

Remote participation:

Title: Nitro Isolation Engine: formally verifying a production hypervisor

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 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.