Hacker News

points by lrvick 1 day ago | 0 comments

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.

https://hypervisor.org/

[–] eddythompson80 1 day ago

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.

[–] markasoftware 1 day ago

Xen had a generic guest to host vulnerability disclosed in the last few days: https://codeant.ai/security-research/xenbleed-a-grant-copy-c...

[–] eddythompson80 1 day ago

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.

[–] markasoftware 1 day ago

Novas core seems to be formally verified which rules out a vast amount of bug categories that can happen with xen, including this one

[–] eddythompson80 1 day ago

Interesting, I'll have to learn more about Nova.

[–] lrvick 1 day ago

See Udos most recent talk at 3mdeb Boot Mastery Conference.

He is an ex Intel CPU engineer and the depth of his thought into the security design had me questioning my life choices.

[–] skinfaxi 1 day ago

https://youtu.be/RbL65gVzhNk for anyone else looking for it

[–] eddythompson80 1 day ago

Thank you. I'll definitely check that out.

[–] zobzu 1 day ago

having worked with AWS, xen had a lot of very bad vulns over its lifetime as well.

there's no magic.

[–] ThePowerOfFuet 1 day ago

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.

[–] lrvick 1 day ago

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.

[–] Melatonic 1 day ago

Isn't VMware also that design ?

[–] josh-wrale 1 day ago

Xen is formally verified?

[–] tptacek 1 day ago

No.

[–] tptacek 1 day ago

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.

[–] lrvick 1 day ago

Nova is L4 inspired, and interchangable with L4 kernels in Genode.

[–] tptacek 1 day ago

Yep, very similar, but L4 is a little bit more general purpose (despite being microscopically tiny) and a little more battle-tested.

[–] lrvick 1 day ago

Is there a well tested L4 hypervisor solution with hardware accelerated virtualization and raw TPM support formally verified to a similar or greater level than Nova with similar remote attestation and security features?

SeL4 is the closest contender on my radar atm.

[–] tptacek 1 day ago

Most of the L4s have hypervisor situations. I don't know about TPM support. Generally the vibe I get from systems security people is a bit of eye-rolling about the formal verification of things like L4; the real win is just drastic attack surface reduction.

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.

[–] lrvick 1 day ago

I for one do not want any code in the TCB that is not formally verified, tiny, and easy to audit with every line of code justified.

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!

[–] tptacek 1 day ago

Like some of what I'm saying is just that if you tell a systems security person "we're using seL4 because of its formal verification", you're going to get eye rolls. Whatever else you want to say about it, the formally-verified configuration of seL4 doesn't actually do much, meaning whatever system you're building on top of it is going to be where all the security drama is anyways.

I'm certainly not telling you to use Xen. I wouldn't use Xen for anything untrusted.

[–] traceroute66 1 day ago

> 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."

[–] lrvick 1 day ago

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.

[–] Melatonic 1 day ago

What's the OS ?

[–] lrvick 6 minutes ago

A remotely attestable hardened server OS based on https://stagex.tools to power https://caution.co . More will be shared when it is a bit more mature :)

[–] tptacek 7 hours ago

It's its own OS.