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.
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.
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?
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.
This is not a new vulnerability, it's just a description of how to exploit the PwnEscape vulnerability in practice on firecracker VMs (disclosed multiple weeks ago and discussed in some less upvoted posts on HN)
The actual vulnerability got very little discussion. It's clever. Because Linux networking people are obsessed with checksum performance, virtio-net plumbs checksum offload metadata through the host/guest driver interface. Guests can thus deliver the host packets along with instructions on what to checksum. The vulnerability is a missing sanity check that allows checksum instructions to instruct the host to overwrite the header length field in the IPv4 header, rather than the checksum field.
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.
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/
This is different from KVM where your hypervisor runs in your Dom0/Root Partition.
Anyone considering Xen should probably also consider Nova depending on requirements.
SeL4 is the closest contender on my radar atm.
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.
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.
(Doesn't HN usually deduplicate links? I'm confused)