AWS Nitro Isolation Engine: Formally verifying the hypervisor in the AWS Nitro System

Post Syndicated from Ali Saidi original https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system/

Ali Saidi is a VP and Distinguished Engineer at AWS

Millions of customers use the AWS Nitro System to protect their most sensitive workloads, and AWS is an industry leader in innovation to secure customer data. Helping our customers keep their data secure and confidential is our highest priority, and we continue to make investments in purpose-built hardware and software for data isolation and protection.

In 2017, AWS launched the Nitro System, the first major cloud platform designed with zero operator access to customer data. The Nitro System is purpose-built hardware and software that provides the foundation for all modern Amazon EC2 instances, offloading virtualization, storage, and networking functions to dedicated hardware and a minimal hypervisor. With the Nitro System, even the most privileged AWS operators are only able to interact with the system via authenticated, audited administrative APIs that cannot access customer workloads. This architecture has set the industry standard for cloud security, and third parties like NCC Group have independently validated our approach.

Now, we’re raising the bar even further. One of the primary responsibilities of the AWS Nitro System is to isolate instances from each other and from AWS operators. This has been a cornerstone of the Nitro System architecture for over a decade. The AWS Nitro Isolation Engine, first announced at re:Invent 2025 and generally available on all Graviton5-based instances starting today, is a purpose-built component within the Nitro Hypervisor responsible for enforcing this isolation and proving it with mathematical precision. Nitro Isolation Engine uses formal verification, a technique to mathematically demonstrate that the hardware or software behaves as intended, and not only in specific test cases. This intensive verification technique establishes Nitro as the first formally verified cloud hypervisor, setting a new standard for mathematically proven cloud security.

AWS Nitro Isolation Engine

Within the Nitro System, the AWS Nitro Hypervisor is designed so that no unauthorized entity can read or modify customer data across all virtual machines. Nitro Isolation Engine is a purpose-built component of the Nitro Hypervisor that enforces isolation between these virtual machines. It mediates all access to virtual machine memory, CPU register state, and I/O devices through a minimal set of APIs that are exposed to the rest of the Nitro Hypervisor. It is the sole system component that mediates access to customer data. The remaining Nitro Hypervisor components must operate through this restricted interface and cannot access customer workloads directly. The Nitro Isolation Engine’s minimalist code base eases human audit, reduces scope for bugs, and makes it feasible to apply formal verification to its design and implementation.

Formal verification

Formal verification uses mathematical proof to demonstrate that properties of a formal model of a system hold true in all possible system states and over all possible inputs. This contrasts with testing, where a system’s behavior is checked against a (potentially large) subset of possible states and inputs. Formal verification provides far stronger evidence about correctness than traditional testing. In the case of Nitro Isolation Engine, our isolation properties are assured across all possible system behaviors. Testing and verification are complementary. Verification extends testing, and testing covers areas of the system not yet verified and builds an intuition that the system is behaving as intended.

For customers, formal verification of the code responsible for enforcing isolation provides assurance beyond comprehensive testing. Testing remains essential, and we maintain a high bar for it — but testing can only check specific scenarios. Formal verification is complementary: it means that isolation properties are mathematically assured across all possible scenarios, not just those covered by testing.

Formally verified properties

The formal verification of the Nitro Isolation Engine establishes four key properties:

1/ Confidentiality and Integrity – The Nitro Isolation Engine preserves the confidentiality and integrity of guest virtual machines (VM). Confidentiality means that a guest VM’s private data cannot be read by any unauthorized entity and Integrity means that a guest VM’s private data cannot be modified by any unauthorized entity.

2/ Functional Correctness – Every verified hypercall matches the expected behavior defined in the specification. The specification captures the preconditions and postconditions of each hypercall, and the proof establishes that the implementation never deviates from them.

3/ Absence of Runtime Errors – The code never encounters runtime errors and the implementation behaves as specified. Together, formal verification of these properties establishes mathematically rigorous assurance that the Nitro System maintains isolation for any sequence of events covered by the verification. Today, the verification covers the hypercalls for the core VM lifecycle responsible for bringing up, running, and tearing down a VM.

4/ Memory Safety – Establishes the absence of memory safety violations such as buffer overflows, NULL pointer dereferences, and out-of-bound access. As is the case for all verified software, the Nitro Isolation Engine proofs are subject to assumptions, such as the correctness of the Rust compiler and hardware. These assumptions and our approach to engineering and verification are detailed further in the Nitro Isolation Engine whitepaper.

Rust implementation

Nitro Isolation Engine is implemented in Rust, a systems programming language designed to prevent common programming pitfalls that have historically been the root cause of security vulnerabilities in sensitive software. The choice of Rust for the Nitro Isolation Engine eliminates entire classes of bugs by construction. What makes Rust a good fit is its type of system — it enforces a strong ownership discipline, which makes some aspects of formal verification easier and provides a first layer of assurance at compile time.

Conclusion

The Nitro Isolation Engine represents our continued commitment to keeping our customers’ data confidential. This is only the starting point. We will continue to extend formal verification across all major components of the Nitro Isolation Engine that impact security and maintain those proofs as new features are introduced. In addition, we plan to make the Nitro Isolation Engine’s source code and formal proofs available to third parties for independent inspection and review. We believe this level of transparency sets a new standard for how cloud providers can demonstrate openness, code quality, and formal verification.

To learn more about the AWS Nitro System and confidential computing, see the following resources:

Noise