EC2's Formally Verified 'Isolation Engine' Provides Mathematical Guarantees for Virtual Machine Isolation

AWS launched new M9g and M9gd instances based on Graviton5, and unveiled the Nitro Isolation Engine, which guarantees isolation between virtual machines (VMs). This engine is a core component of the Nitro Hypervisor, and is the first Formally Verified hypervisor deployed in a commercial cloud environment.

This verification was performed using the Isabelle/HOL proof assistant tool, and includes approximately 330,000 lines of machine-verified mathematical proof. This is comparable in scale to the seL4 project, a milestone in operating system verification. AWS applied the 'Separation Kernel' concept, which minimizes isolation logic, extracting only the core isolation logic from the complex Nitro Hypervisor to increase verifiability.

Key features of the verification process are as follows:

• Implemented using the Rust language, achieving a structure optimized for formal verification
• Formalization performed on μRust (a core subset of Rust)
• Utilization of Separation Logic and the AutoCorrode library
• Verification of four core properties: confidentiality and integrity, functional correctness, absence of runtime errors, and memory safety

The Nitro Isolation Engine is provided as an always-on feature for Graviton5 users, offering customers unprecedented transparency into isolation mechanisms.