Comment by lrvick
21 hours ago
I am more convinced by the day that the Nova Microhypervisor approach is correct.
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.
How is this different from Xen? It's the same approach as Xen or Hyper-V where the hypervisor is its own component, then you boot into a virtualized Dom0 or Root Partition (in Xen and Hyper-V terminology respectively) that can manage the hypervisor underneath it.
This is different from KVM where your hypervisor runs in your Dom0/Root Partition.
Xen had a generic guest to host vulnerability disclosed in the last few days: https://codeant.ai/security-research/xenbleed-a-grant-copy-c...
Yeah, all security design guarantees are as good as the implementation at the end of the day. All the fancy hashing and encryption math in the world isn't gonna save you from an erroneous `"" == ""` check or an invalid reference check.
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.
5 replies →
having worked with AWS, xen had a lot of very bad vulns over its lifetime as well.
there's no magic.
Now compare to Linux, which is the point raised. Nobody said alternatives like Xen are perfect... but my oh my, some are much better in this regard.
This is a much lighter weight (~100k) alternative to Xen focused on baremetal TPM anchored remote attestation, formal verification, and trusted computing applications.
Anyone considering Xen should probably also consider Nova depending on requirements.
Isn't VMware also that design ?
Xen is formally verified?
No.
I don't know much of anything about Nova but since the late 1990s this has also been the pitch for L4; there are several mature L4's.
Nova is L4 inspired, and interchangable with L4 kernels in Genode.
Yep, very similar, but L4 is a little bit more general purpose (despite being microscopically tiny) and a little more battle-tested.
9 replies →
[dead]
> the Nova Microhypevisor approach is correct
To save people the time:
"This code is experimental and not feature complete. If it breaks, you get to keep both pieces."
The actual main open source repo has had that warning there for 14 years in spite of commercial forks that are deployed in production government and high risk use cases.
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.
What's the OS ?
[flagged]
That phrase predates LLMs.
Considering the commit that added that text was 14 years ago, I am going to assume it was written by a human.
https://github.com/udosteinberg/NOVA/commit/9e35d89c0e7014f1...