[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Dear colleagues,
At AWS re:Invent 2025 in Las Vegas, we announced the AWS Nitro Isolation Engine
[1, 2, 3], a formally verified enhancement to the AWS Nitro System that
enforces isolation between virtual machines hosted on AWS's new Graviton5-based
EC2 instances.
Nitro Isolation Engine represents a significant deployment of mechanized proof
in production infrastructure, and we therefore wanted to bring this to the
attention of the formal methods and programming languages communities. This
work builds directly on decades of advances in interactive theorem proving,
program verification, and programming languages theory, alongside landmark
projects—such as, seL4 [4], CertiKOS [5], SeKVM [6], and many others—that were
inspirations for this work.
What is Nitro Isolation Engine?
Nitro Isolation Engine is a small, trusted computing base written in Rust that
sits beneath the AWS Nitro Hypervisor, providing a security isolation boundary
between the hypervisor and guest virtual machines, and between co-tenanted
guest virtual machines. The Nitro Isolation Engine controls the critical
hardware features required for isolating customer workloads, primarily control
of Stage Two translation tables.
The verification effort
Nitro Isolation Engine was designed with verification in mind from the first
line of code. Nitro Isolation Engine is subject to AWS’s existing rigorous
engineering practices, including the deployment of property-based-testing and
lightweight formal methods, for example the Kani bounded model checker for Rust
[7].
Building atop this foundation, we have specified and verified the correctness
of Nitro Isolation Engine in Isabelle/HOL [8]. Our model and proofs consist of
around 260,000 lines of machine-checked models and proofs. Specifically, we
have proved:
* Functional correctness: Nitro Isolation Engine behaves as specified for
all operations: virtual machine creation, memory mapping, instruction and data
abort handling, and so on. As corollaries of our total verification style, we
have also proven memory-safety, termination, and absence of runtime errors,
providing our modelling assumptions are accurate.
* Confidentiality: We prove a noninterference-style property demonstrating
the confidentiality of guest virtual machine states, formalized as
indistinguishability preservation up-to permitted flows of declassified
information out of a guest.
* Integrity: The integrity of guest virtual machine state is formalized as
a safety property, showing that the private state of one virtual machine is
unaffected by operations modifying another distinct virtual machine.
In addition, we have applied Iris [9] and Verus [10] to prove the correctness
of the Nitro Isolation Engine’s concurrency primitives, including ticket locks,
mutexes, and rendezvous barriers.
For functional verification, we defined μRust, a restricted subset of Rust
expressive enough to write Nitro Isolation Engine but amenable to formal
reasoning and embedded its semantics into Isabelle/HOL. Specifications are
written in separation logic, and proofs proceed via weakest precondition
calculus with custom automation. We have made our verification infrastructure
open source as the AutoCorrode library [11] for Isabelle/HOL, which may be of
independent interest.
Regards,
Automated Reasoning Group, AWS
[1]:
https://urldefense.com/v3/__https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hEobcjHk$
[2] :
https://urldefense.com/v3/__https://www.youtube.com/watch?v=3Gt-30Fm38U__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hZrhHvVs$
https://urldefense.com/v3/__https://www.youtube.com/watch?v=3Gt-30Fm38U__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hZrhHvVs$
<https://urldefense.com/v3/__https://www.youtube.com/watch?v=3Gt-30Fm38U__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hZrhHvVs$
>
[3]:
https://urldefense.com/v3/__https://www.youtube.com/watch?v=b0P55gHhG4g__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hGGeL7T0$
[4]:
https://urldefense.com/v3/__https://sel4.systems/__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hu8XQA40$
[5]:
https://urldefense.com/v3/__https://flint.cs.yale.edu/certikos/__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hEnkH-mA$
[6]:
https://urldefense.com/v3/__https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hvNoNgSY$
[7]:
https://urldefense.com/v3/__https://github.com/model-checking/kani__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hoCrbNCI$
[8]:
https://urldefense.com/v3/__https://isabelle.in.tum.de/__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hrZSjcw8$
[9]:
https://urldefense.com/v3/__https://iris-project.org/__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hn0WPe4Y$
[10]:
https://urldefense.com/v3/__https://github.com/verus-lang/verus__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hqnfdyqc$
[11]:
https://urldefense.com/v3/__https://github.com/awslabs/AutoCorrode__;!!IBzWLUs!WFMgR7uzNXdIKtLVBjLs6mCoeRMP3C3rJAhx_TLHN3yA1HCiGnp6zqyUxqfQZpcjgN5qkhcXA0nFVJ43vhaV2u6hzMW76rw$
