EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
Captured source
source ↗How formal verification makes AWS Nitro the first formally verified cloud hypervisor - Amazon Science
Close
Close
Social
bluesky
threads
youtube
github
rss
Menu
Research
Research areas
Automated reasoning
Cloud and systems
Computer vision
Conversational AI
Economics
Information and knowledge management
Machine learning
Operations research and optimization
Quantum technologies
Robotics
Search and information retrieval
Security, privacy, and abuse prevention
Sustainability
Our scientific contributions
Publications
Research from our scientists and collaborators.
Conferences
Our experts present and discuss cutting-edge research at scientific meetings globally.
Research areas
Automated reasoning
Cloud and systems
Computer vision
Conversational AI
Economics
Information and knowledge management
Machine learning
Operations research and optimization
Quantum technologies
Robotics
Search and information retrieval
Security, privacy, and abuse prevention
Sustainability
Our scientific contributions
Publications
Research from our scientists and collaborators.
Conferences
Our experts present and discuss cutting-edge research at scientific meetings globally.
News & blog
The latest from Amazon researchers
Amazon Science Blog
Technical deep-dives and perspectives from our scientists.
News
Research milestones and recent achievements.
The latest from Amazon researchers
Amazon Science Blog
Technical deep-dives and perspectives from our scientists.
News
Research milestones and recent achievements.
Collaborations
Amazon Research Awards
Overview
Call for proposals
Latest news
Research stories
Recipients
Amazon Nova AI Challenge
Overview
Rules
FAQs
Teams
Research collaborations
Overview
Carnegie Mellon University
Columbia University
Hampton University
Howard University
IIT Bombay
Johns Hopkins University
Max Planck Society
MIT
Tennessee State University
University of California, Los Angeles
University of Illinois Urbana-Champaign
University of Southern California
University of Texas at Austin
Virginia Tech
University of Washington
Amazon Research Awards
Overview
Call for proposals
Latest news
Research stories
Recipients
Amazon Nova AI Challenge
Overview
Rules
FAQs
Teams
Research collaborations
Overview
Carnegie Mellon University
Columbia University
Hampton University
Howard University
IIT Bombay
Johns Hopkins University
Max Planck Society
MIT
Tennessee State University
University of California, Los Angeles
University of Illinois Urbana-Champaign
University of Southern California
University of Texas at Austin
Virginia Tech
University of Washington
Resources
Code and datasets
AGI Labs
Meet the team building useful AI agents.
Amazon Nova
Try Amazon’s frontier foundation models.
Code and datasets
AGI Labs
Meet the team building useful AI agents.
Amazon Nova
Try Amazon’s frontier foundation models.
Careers
Careers
Explore our open roles.
Amazon Scholars
Faculty research opportunities on industry-scale technical challenges.
Postdoctoral Science Program
Early-career research opportunities alongside experienced industry scientists.
Careers
Explore our open roles.
Amazon Scholars
Faculty research opportunities on industry-scale technical challenges.
Postdoctoral Science Program
Early-career research opportunities alongside experienced industry scientists.
Search
Submit Search
Automated reasoning
EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation
Splitting the “separation kernel” off from the rest of the Nitro security system and using only a subset of the Rust programming language to code it enabled its formal verification.
By Dominic Mulligan , Nathan Chong
June 10, 2026
7 min read
Share
Share
Copy link
X
Line
QZone
Sina Weibo
分享到微信
x
Overview by Amazon Nova
The Nitro Isolation Engine is the core component of the Nitro Hypervisor, the first formally verified hypervisor deployed in a commercial cloud environment, ensuring correct behavior and enforcement of isolation between virtual machines. The formal verification of the Nitro Isolation Engine was achieved using the Isabelle/HOL proof assistant, resulting in 330,000 lines of machine-checked mathematics, comparable in scale to the seL4 project. The verification process involved creating a formalization of a core subset of the Rust language (μRust), using Separation Logic for specifications, and applying weakest-precondition calculus for proofs, all part of the open-sourced AutoCorrode library. The verification addressed four types of properties: confidentiality and integrity, functional correctness, absence of runtime errors, and memory safety, with confidentiality and integrity treated separately using noninterference and indistinguishability preservation. The Nitro Isolation Engine is designed for a commercial cloud environment and is an always-on feature for Graviton5 users, providing unprecedented visibility into how isolation is enforced.
Was this answer helpful?
Today we announced the general availability of the new M9g and M9gd instances of Amazon Web Services’ (AWS’s) Elastic Compute Cloud (EC2), the first instance types powered by Graviton5, the latest generation of our general-purpose CPU. Graviton5 doubles the number of cores from the previous generation, from 96 to 192. They’re also the first instance types to use the new Nitro Isolation Engine, a component of the Nitro Hypervisor whose sole job is isolating virtual machines (VMs) from each other. In this post, we explain how we used the Isabelle/HOL (higher-order logic) proof assistant — software that mechanically checks reasoning steps for adherence to the laws of logic — to prove that the Nitro Isolation Engine behaves correctly and enforces isolation between virtual machines. The Nitro Isolation Engine is the critical component of the first formally verified hypervisor to be deployed in a commercial cloud environment. Our Isabelle/HOL model and proof comprise 330,000 lines of machine-checked mathematics. It’s comparable in scale to seL4 , the landmark project that first demonstrated that realistic operating-system verification was feasible and was an inspiration for our own work. However, unlike seL4, the Nitro Isolation Engine is designed for a commercial cloud environment and ships on...
Excerpt shown — open the source for the full document.
Notability
notability 1.0/10Not an AI event