Nitro Isolation Engine: formally verifying a production cloud hypervisor

ABSTRACT

Cloud computing fundamentally relies on hypervisors to enforce isolation between co-tenanted virtual machines. Cloud hypervisors
are therefore critical security infrastructure, and assurance of their correctness is paramount. This technical talk presents the techniques and
methods that we have used in an industrial setting to formally verify
a production hypervisor component, the Nitro Isolation Engine: a new,
minimal, trusted computing base written in Rust that enforces isolation
between virtual machines. The Nitro Isolation Engine is in production in Amazon EC2 (Elastic Compute Cloud) as a default, always-on capability of Graviton5-based instances¹.

Designed with verification from inception, we have formally specified the Nitro Isolation Engine and proven functional correctness and security properties in the Isabelle/HOL interactive theorem prover. Currently our proof effort is approximately 260K 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, formalized as indistinguishability preservation up to permitted declassification flows
• Integrity: Guest virtual machine private state is unaffected by operations on distinct virtual machines.

This talk will cover our verification approach and the key proof techniques and methods that have worked in practice in our industrial setting.

--

¹https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2

BIOS

Nathan Chong is a Principal Applied Scientist at Amazon Web Services. His work focuses on specification and verification at the hardware/software boundary. Prior to AWS, he was a Principal Researcher at Arm. He has a PhD from Imperial College London on scalable verification techniques for GPU programs.

Robert Dockins is currently an applied scientist at Amazon Web Services. He specializes in program verification and interactive theorem proving, and his recent work has focused on proving the correctness and security of the Nitro Isolation Engine.

Robert received his doctorate degree from Princeton University in 2012, working on what would become the Verified Software Toolchain under the advice of Andrew Appel. He held a postdoc position at Portland State University before joining Galois in 2014, where he remained until joining AWS in 2022.