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 and is a default, always-on capability of Graviton5. 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]