VOOZH about

URL: https://thenewstack.io/graviton5-nitro-isolation-engine/

⇱ AWS can now mathematically prove your VMs are isolated - The New Stack


TNS
SUBSCRIBE
Join our community of software engineering leaders and aspirational developers. Always stay in-the-know by getting the most important news and exclusive content delivered fresh to your inbox to learn more about at-scale software development.
REQUIRED
It seems that you've previously unsubscribed from our newsletter in the past. Click the button below to open the re-subscribe form in a new tab. When you're done, simply close that tab and continue with this form to complete your subscription.
The New Stack does not sell your information or share it with unaffiliated third parties. By continuing, you agree to our Terms of Use and Privacy Policy.
Welcome and thank you for joining The New Stack community!
Please answer a few simple questions to help us deliver the news and resources you are interested in.
REQUIRED
REQUIRED
REQUIRED
REQUIRED
REQUIRED
Great to meet you!
Tell us a bit about your job so we can cover the topics you find most relevant.
REQUIRED
REQUIRED
REQUIRED
REQUIRED
REQUIRED
Welcome!

We’re so glad you’re here. You can expect all the best TNS content to arrive Monday through Friday to keep you on top of the news and at the top of your game.

What’s next?

Check your inbox for a confirmation email where you can adjust your preferences and even join additional groups.

Follow TNS on your favorite social media networks.

Become a TNS follower on LinkedIn.

Check out the latest featured and trending stories while you wait for your first TNS newsletter.

PREV
1 of 2
NEXT
VOXPOP
As a JavaScript developer, what non-React tools do you use most often?
Angular
0%
Astro
0%
Svelte
0%
Vue.js
0%
Other
0%
I only use React
0%
I don't use JavaScript
0%
Thanks for your opinion! Subscribe below to get the final results, published exclusively in our TNS Update newsletter:
NEW! Try Stackie AI
From clobbered drafts to real-time sync
Apr 14th 2026 10:00am, by David Moore
TypeScript 6.0 RC arrives as a bridge to a faster future
Mar 14th 2026 9:00am, by Darryl K. Taft
Mastra empowers web devs to build AI agents in TypeScript
Jan 28th 2026 11:00am, by Loraine Lawson
2026-06-10 12:46:34
AWS can now mathematically prove your VMs are isolated
Containers / Science

AWS can now mathematically prove your VMs are isolated

AWS Graviton5 is now GA with 192 cores, 35% faster ML inference, and a formally verified Nitro Isolation Engine for stronger VM security.
Jun 10th, 2026 12:46pm by Frederic Lardinois
👁 Featued image for: AWS can now mathematically prove your VMs are isolated

On Wednesday, AWS announced that its Graviton5 processor is now generally available and powers two new Amazon EC2 instances: M9g for general-purpose workloads and M9gd for workloads that require high-speed local storage. These are the first Graviton5 instances since AWS previewed the chips at re:Invent 2025.

The new chips double Graviton4’s core count from 96 to 192, and AWS says the new instances will deliver up to 25% better compute performance than the previous generation. 

AWS says the new instances will deliver up to 25% better compute performance than the previous generation. 

What’s maybe more interesting, however, is that these new instances also run on the sixth-generation Nitro System, which now includes the Nitro Isolation Engine, a new, formally verified security component that AWS describes as “a separation kernel whose sole job is isolating virtual machines from each other.”

A kernel whose only job is isolation

The idea of a separation kernel has been around for a while. John Rushby coined the term in 1981. His core idea was that a standard OS kernel, even at the time, had become far too large to formally verify. A smaller, specialized separation kernel, however, would still allow formal verification due to its relatively limited complexity.

AWS launched its Nitro system and hypervisor in 2017, and it has enforced isolation in EC2 ever since. But Nitro also handles substantial business logic and manages device drivers and other AWS-specific features, meaning it was not designed for formal verification from the start.

With this new system, the Nitro hypervisor still handles policy, including VM creation, resource allocation, migration, and scheduling, but it is now somewhat deprivileged and must ask the Nitro Isolation Engine (NIE) to perform any operation that touches guest state, and the Isolation Engine checks every request before acting.

“Distilling the hypervisor’s security-critical isolation logic into a minimal component, the NIE, makes it small enough to verify and audit, giving customers unprecedented visibility into how isolation is enforced,” AWS’s Dominic Mulligan and Nathan Chong write. “We also wrote NIE in Rust, a language that lends itself more naturally to formal verification.”

How we got here

Some of the earlier work in this area includes Columbia’s SeKVM project, which was the first formally verified commercial-grade hypervisor in 2021. But it looks like this was mostly a research project that never ran in a commercial cloud. 

AWS itself credits seL4, a project that demonstrated that OS verification was feasible. 

To prove the kernel behaves correctly, AWS used the Isabelle/HOL proof assistant. AWS says the model and proof “comprise 330,000 lines of machine-checked mathematics,” making it comparable to the seL4 project. “However, unlike seL4, NIE is designed for a commercial cloud environment and ships on production hardware as an always-on feature for Graviton5 users,” AWS writes in its announcement.

192 cores: a substantial redesign

The chip itself got a substantial redesign. Graviton5 moves from TSMC’s 4nm process to 3nm, and while Graviton4 put all 96 cores on a single chiplet with PCIe and DDR controllers on their own chiplets, Graviton5 divides its 192 cores across four chiplets, each with its own controllers, which puts the memory controllers closer to the cores. 

AWS claims that, together with faster memory chips, this will allow web applications to run up to 35% faster and ML inference up to 35% faster than on Graviton4. 

Graviton and agentic AI

AWS positions Graviton5 as purpose-built for agentic AI. That pitch, which isn’t all that different from Google’s pitch for its ARM processors, seems to be working. Meta signed a multibillion-dollar agreement in April to deploy tens of millions of Graviton cores for its agentic AI work, and Snowflake committed $6 billion over five years in May. AWS says Uber is also deploying Graviton for agentic workloads.

In total, AWS says, more than 120,000 customers currently use Graviton, and that more than half of new CPU capacity added to AWS has been Graviton for the third year running. 

AWS may have a bit of an early mover advantage here. Microsoft’s Cobalt 200 is still in preview, Google’s latest Axion chips only went GA in January, and Nvidia’s Vera — maybe the most hyped of all of these chips — will arrive in the second half of the year.

TRENDING STORIES
Before joining The New Stack as its senior editor for AI, Frederic was the enterprise editor at TechCrunch, where he covered everything from the rise of the cloud and the earliest days of Kubernetes to the advent of quantum computing....
Read more from Frederic Lardinois
SHARE THIS STORY
TRENDING STORIES
SHARE THIS STORY
TRENDING STORIES
TNS DAILY NEWSLETTER Receive a free roundup of the most recent TNS articles in your inbox each day.
The New Stack does not sell your information or share it with unaffiliated third parties. By continuing, you agree to our Terms of Use and Privacy Policy.