EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation

Summary

AWS has introduced M9g and M9gd EC2 instances powered by Graviton5 CPUs, featuring the formally verified Nitro Isolation Engine to enforce virtual machine isolation. To prove the engine's correctness, engineers developed 330,000 lines of machine-checked mathematics using the Isabelle/HOL proof assistant. The system architecture separates hypervisor policy from isolation mechanisms, requiring the deprivileged Nitro Hypervisor to route all guest state modifications through the minimal Rust-based engine. Functional verification uses a restricted language subset called micro Rust, Separation Logic contracts specifying total correctness, and weakest-precondition calculus from the open-source AutoCorrode library. Finally, high-level transition relations and noninterference proofs ensure that memory integrity and guest confidentiality are preserved across every execution step.

Takeaways

1. 1

   The Nitro Isolation Engine decouples isolation mechanisms from policy logic, leaving VM creation, resource allocation, and scheduling to the deprivileged Nitro Hypervisor.

2. 2

   AWS formalized micro Rust, a restricted subset of Rust excluding traits and dynamic dispatch, with shallow embedding in Isabelle/HOL to make low-level code amenable to formal proofs.

3. 3

   Confidentiality and integrity are mathematically guaranteed through noninterference, ensuring that two indistinguishable system states remain indistinguishable after state transitions.