Do virtualization with a tiny formally verified microkernel and have complex kernels like Linux run underneath instead of letting a huge, complex, and brittle linux kernel and vm ecosystem control the hypervisor layer.
This is different from KVM where your hypervisor runs in your Dom0/Root Partition.
I was replying to OP saying it's the same "approach" as Xen, if your preference is "approach" based. It's fair though to point to Nova's smaller code base. It's becoming an important metric for me in general (how big is the code base). It's not a bullet proof thing, but having a smaller code base is a positive sign in 2026 for me.
SeL4 is the closest contender on my radar atm.
And then, of course, L4s live in millions and millions of shipped products, which is a reason to consider L4 instead of something novel, but I'm not saying you should or shouldn't.
SeL4 is the only open, mature, and formally verified L4 solution I am aware of that can run on modern servers, but IIRC given vCPUs are not first class objects and any low level CPU virtualization features are handled in user space, it comes at a real performance cost making it only suitable for single-core or non-performance-critical applications.
Nova by contrast was built to handle the expensive and trust critical TPM and vCPU handling directly for high performance remotely attestable multi-core applications without having to reach for something as heavy as Xen, though formal verification is admittedly not as complete as SeL4 yet AFAICT, though lots of recent progress here.
Those are pretty big tradeoffs, but if you or anyone else knows other viable xen alternatives this general shape with a tiny easily-auditable footprint, please chime in!
I'm certainly not telling you to use Xen. I wouldn't use Xen for anything untrusted.
As a systems security engineer myself I would disagree and know several others that would as well. All depends on your circles, applications, and threat model I suppose.
Xen, Hyper-V, and KVM have all had major security flaws in the form of logic violations, spacial memory corruptions, use-after-free, and pointer corruptions that allowed hypervisor trust boundary violations. I expect most if not all of those classes of bugs could have been prevented by formal verification.
Xen likely has a bad reputation with both of us because of a history of preventable flaws like these.
In my applications every single daemon gets its own sandbox, which is a VM whenever possible. Some with network, some without network, different filesystem and vsock access for maximum damage control and minimal trust between daemons. The hypervisor is the most important security boundary to me especially when isolating user-controlled workloads. The more confidence I can get that it is correct the better.
Not my intent but perhaps I communicated poorly. It was an argument that the -reason- Xen has had so many bugs is because it was not built for correctness.
Formal verification should be a bare minimum for a TCB component to know many classes of bugs that have plagued the most popular hypervisors cannot happen.
We both clearly agree not to use Xen.
Anyway, I appreciate the engagement on this all the same.
Few even know alternatives to xen exist!
Generally, the less your OS can do, apart from strictly hypervising guest operating systems, the safer you probably are. Hence why people do things like seL4.
100% agreement here and I -would- take something tiny I can audit myself over something huge and formally verified if forced to choose. Thankfully I do not have to choose.
> AI lets us be more ambitious with verification
Exactly. For TCB code formal verification is a minimum, not sufficient, IMO. Too cheap these days to not have very complete test coverage, formal verification, risc0 execution proofs, seccomp tracing. For security critical code we should demand all of it now.
To save people the time:
"This code is experimental and not feature complete. If it breaks, you get to keep both pieces."
See his latest talk which represents a lot of impressive recent work: https://cfp.3mdeb.com/media/bsmconf/submissions/KW3SYT/resou...
I am working on a production OS using it as a foundation.
https://github.com/udosteinberg/NOVA/commit/9e35d89c0e7014f1...
It hosts hundreds of database engines - many of them have vulnerabilities, and some of them, like Pandas, are basically open RCEs regardless.
We can PoC the Firecracker VM Escape on that service.
> "run SQL against 110+ databases"
I work on connectors for datasources (mostly DB's. Being able to quickly test things like sorting behavior and how the same function can be emulated across DB's would have made my life so much easier.
Couldn't find it. Care to provide link.
Crucially, this happens in the middle of packet processing, so the kernel code is forced to work with two different ideas of how long the IPv4 header is. All hell predictably breaks loose.
https://github.com/torvalds/linux/commit/6785011f8b16abf40b1...
(Doesn't HN usually deduplicate links? I'm confused)
Running our microVM's inside of a jailed zone, at least gives me some peace of mind.. It's far from perfect, as a zone escape could be lurking.. but at least it's a layer of defense.
How do people feel about the hardware isolation provided by microVMs versus the stronger end of software isolation techniques like gvisor?
Right now, we put a huge amount of stock in "hardware isolation". If that starts falling to agents to any substantial degree, I wonder whether we might end up leaning more on patchable software isolation, similar to the rise of software RAID (though, in userspace this time).
> The configuration used here had no jailer. Firecracker's production containment includes dropping privileges and restricting the process through namespaces and seccomp. A deployment using those controls requires a separate assessment of the privileges and resources available after compromising its VMM.
If I'm understanding all of this correctly, a properly jailed and configured firecracker instance would greatly reduce the blast radius of this escape, and I feel as though it would have been good for them to explain what jailing and dropping privileges would do to help. I'd hope most production firecracker deployments would be doing this already.
Not saying that this is any less severe and the root issue is not specific to Firecracker, but to a flaw in the kernel's network code -- they just used an insecure firecracker configuration to demonstrate it. However, I feel like some are taking this as a flaw with firecracker when its not. This is an issue in the kernel networking stack.
Another wave of vulnerabilities like this are yet to be discovered in Linux. We are just seeing how weak C and C++ based OSes and kernels are when put under hundreds of AI agents.
[0] https://openai.com/index/a-thousand-fewer-paths-to-root/
The only reason it wasn't seen as a problem was due to the effort and time it took to find and exploit them.
Exactly, its not a firecracker issue. Using firecracker without a jailer is like setting your password to "password".
This is a really good bug and nobody should downplay it.
Which like, isn't really a proof of concept of anything being described.
"That was always allowed".
It just bothers me that the proof of concept starts with the assumption that host physical memory is mapped into guest physical memory at 2^39. If you can't talk about the actual exploit yet, I get it , but don't write a blog post with something like that called a "proof of concept" when the code shows no exploit, and you're obviously dancing around the actual novel exploit here in the chain. Just keep it in your pants until the disclosure window.