Click any tag below to further narrow down your results
Links
AWS introduced the Nitro Isolation Engine on its new M9g and M9gd Graviton5 instances and used Isabelle/HOL to prove that it enforces strict VM isolation. They modeled the engine in a subset of Rust (μRust), wrote Separation Logic specifications, and proved functional correctness, memory safety, and noninterference to guarantee confidentiality and integrity.
- AWS deployed a formally verified hypervisor component (Nitro Isolation Engine) into production commercial cloud infrastructure for the first time, on new M9g/M9gd Graviton5 instances.
- They produced 330,000 lines of machine-checked Isabelle/HOL proofs, matching seL4's verification scale, covering functional correctness, memory safety, and noninterference.
- The proof approach modeled the engine in a custom μRust subset (no traits/dynamic dispatch) with Separation Logic specs and a weakest-precondition calculus via their open-source AutoCorrode library.
- Every guest-state-touching operation must pass through this engine, which checks requests against the formal spec to mathematically guarantee VM confidentiality and integrity.