Hacker News new | past | comments | ask | show | jobs | submit
lrvick | on: Firecracker VM Escape: PwnEscape Part 2
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 | parent | next
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 | root | parent | next
Xen had a generic guest to host vulnerability disclosed in the last few days: https://codeant.ai/security-research/xenbleed-a-grant-copy-c...
loading story #50398445
loading story #50402023
loading story #50398782
lrvick | root | parent | next
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 | root | parent | next
Isn't VMware also that design ?
josh-wrale | root | parent
Xen is formally verified?
loading story #50400857
tptacek | parent | next
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 | root | parent | next
Nova is L4 inspired, and interchangable with L4 kernels in Genode.
loading story #50398199
traceroute66 | parent
> 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 | root | parent | next
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.

lwansbrough | root | parent
[flagged]
dexter0 | root | parent | next
That phrase predates LLMs.
lrvick | root | parent
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...