EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
Summary
AWS describes EC2’s Nitro Isolation Engine, a formally verified separation kernel embedded in Nitro Hypervisor. The verification, using Isabelle/HOL and μRust, comprises about 330,000 lines of machine-checked math to prove confidentiality, integrity, functional correctness, and memory safety in a commercial cloud context. The work opens AutoCorrode and demonstrates how formal methods are applied to cloud security and isolation.