AWS re:Invent 2025 - Introducing Nitro Isolation Engine: Transparency through Mathematics

The AWS Nitro System

Origins and Evolution

• The AWS Nitro system is the underlying platform that powers all virtualization in AWS EC2 since 2018
• It was developed starting in 2012 to enhance security, performance, cost-efficiency, and innovation in EC2
• Key steps in the Nitro system evolution:
  • Offloading VPC networking and EBS storage to dedicated hardware
  • Replacing the Zen hypervisor with a custom Nitro hypervisor based on KVM

Key Nitro System Features

• Secure boot process with hardware root of trust
• Live updates without impacting customer performance
• Transparent encryption of storage, networking, and memory
• Absolute isolation - no AWS operator access to customer instances

Nitro Hypervisor Design

• Deliberately minimized and customized for AWS use cases
• Functions more like firmware than traditional software
• Primary responsibilities are resource partitioning and isolation between co-tenants

Nitro "Secret Hiding" Approach

• Differs from traditional hypervisors with hierarchical memory model
• Nitro hypervisor cannot access guest data as it's not present in its virtual address space

Introducing the Nitro Isolation Engine

Key Features

1. Compartmentalization: Isolates all confidentiality-related functionality into a separate codebase
2. Formal Verification: Uses automated reasoning and mathematical proofs to provide strong assurance of isolation
3. Transparency: AWS will provide customer access to the Nitro Isolation Engine and associated formal proofs

Engineering Approach

• Demotes the Nitro hypervisor to a lower privilege level
• Nitro Isolation Engine takes on sole responsibility for all isolation and confidentiality
• Communicates with hypervisor via well-defined hypercalls

Formal Verification Process

• Integrates formal proofs into every step of the development lifecycle
• Defines formal mathematical specifications of desired behaviors
• Proves implementation matches specifications using interactive theorem prover (Isabelle)
• Covers memory safety, absence of runtime errors, functional correctness, and information flow control

Technical Foundations

1. Memory Isolation: Hypervisors use virtual memory and MMU to partition physical memory
2. Exception Levels: Hardware-defined privilege levels with restricted access and communication channels
3. Principle of Least Privilege: Only granting the minimum permissions required for correct operation

Formal Proof Guarantees

• Prove memory safety of both safe and unsafe Rust code
• Prove unreachability of runtime errors
• Prove functional correctness of the implementation
• Prove confidentiality and integrity of guest VM data

Key Takeaways

• The Nitro Isolation Engine represents a major evolution in the Nitro system, providing the world's first formally verified hypervisor for cloud computing.
• Formal verification is integrated throughout the entire development process, raising the bar for correctness and security assurance.
• AWS is committed to providing transparency by enabling customer access to the Nitro Isolation Engine implementation and formal proofs.
• This advancement in confidential computing protection demonstrates AWS's continued leadership in cloud security innovation.