Cloud computing relies on hypervisors to enforce safe and performant isolation of co-tenanted virtual machines (VMs). As a result, hypervisors are critical security infrastructure and assurance of their correctness is crucial.

This tutorial is a hands-on deep dive into the verification of the AWS Nitro Isolation Engine: a new, minimal trusted computing base written in Rust that enforces isolation between VMs. The Nitro Isolation Engine was designed from inception with formal verification in mind and we have applied Interactive Theorem Proving using Isabelle/HOL to specify and verify functional correctness and isolation properties. We establish three key classes of property:

1. Functional correctness: the system behaves as specified. Our total verification approach additionally establishes memory-safety, termination, and absence of runtime errors.
2. Confidentiality: A noninterference-style property demonstrates that VM state remains secret with respect to a definition of an observer, formalized as indistinguishability preservation up to permitted declassification flows.
3. Integrity: Private VM state is unaffected by operations on distinct virtual machines. The tutorial will be a mix of talks from the organizers and hands-on keyboard interactive theorem proving using examples from the Nitro Isolation Engine. Attendees will come away with an understanding of the high-level structure of the proof results as well as experience working on real-world examples from the project.

Agenda

• Introduction to the Nitro Isolation Engine, covering the main design and implementation required to understand the rest of the tutorial, which focuses on proof [30min]
• Proof overview, covering the high-level structure of the proof results [30m]
• Reasoning about Rust using AutoCorrode and hands-on exercise [1h]
• Proving confidentiality with hands-on exercise [1h]