Email Gateway (Dec 09 2025 at 16:17): Email Gateway (Dec 09 2025 at 16:17):From: Dominic Mulligan <cl-isabelle-users@lists.cam.ac.uk>
Dear fellow Isabelle users,
(Larry has already kindly pointed to some posts/videos related to this
project a few days ago. This posting provides a bit more information.)
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://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
[2] : https://www.youtube.com/watch?v=3Gt-30Fm38U
https://www.youtube.com/watch?v=3Gt-30Fm38U
<https://www.youtube.com/watch?v=3Gt-30Fm38U>
[3]: https://www.youtube.com/watch?v=b0P55gHhG4g
[4]: https://sel4.systems/
[5]: https://flint.cs.yale.edu/certikos/
[6]:
https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei
[7]: https://github.com/model-checking/kani
[8]: https://isabelle.in.tum.de/
[9]: https://iris-project.org/
[10]: https://github.com/verus-lang/verus
[11]: https://github.com/awslabs/AutoCorrode
Email Gateway (Dec 09 2025 at 16:23):From: David Cock <david.cock@inf.ethz.ch>
Hey, just wanted to extend a really big congratulation to you all.
Knowing from personal experience what it takes to pull something like
this off, this is a really impressive effort. Well done guys!
David
On 12/9/25 17:16, Dominic Mulligan (via cl-isabelle-users Mailing List)
wrote:
Dear fellow Isabelle users,
(Larry has already kindly pointed to some posts/videos related to this
project a few days ago. This posting provides a bit more information.)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://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
[2] : https://www.youtube.com/watch?v=3Gt-30Fm38U
https://www.youtube.com/watch?v=3Gt-30Fm38U
<https://www.youtube.com/watch?v=3Gt-30Fm38U>
[3]: https://www.youtube.com/watch?v=b0P55gHhG4g
[4]: https://sel4.systems/
[5]: https://flint.cs.yale.edu/certikos/
[6]:
https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei
[7]: https://github.com/model-checking/kani
[8]: https://isabelle.in.tum.de/
[9]: https://iris-project.org/
[10]: https://github.com/verus-lang/verus
[11]: https://github.com/awslabs/AutoCorrode
Last updated: Dec 21 2025 at 20:24 UTC