Show HN: L4ES – verifiable Linux microVMs powered by seL4
l4es.dev
l4es.dev
Also wondering a bit how your HV looks at DMA capable devices. does it restrict DMA apertures based on some policies or so in order to ensure they can only write/read certain places? how is that managed if so? theres multiple angles where TPM/secure boot might not be enough. you can use iommu and things like amd-vi to highly restrict these types of devices and interactions.
other then that super cool project really. Like to see a HV being built on Sel4 its a very nice base to build up from if formal verification is your goal.
> what exactly is verified vs. verifiable concerning the hosted linux kernels
We don't really have a fully formally verified hypervisor - SMP verification is not done on seL4 and AFAIK it's hard. And userspace verification is another story :) Verifiable here just means that we have a very small TCB that passes hardware-based trust (e.g. TPM / SEV-SNP) to guest VMs, so that users can verify their VMs are not tampered with.
> how your HV looks at DMA capable devices
We manage VT-d / AMD-Vi IOMMU in the root process. The processes that handles both untrusted guest data and DMA (blkd/netd) only start after IOMMU initialization completes. Guest VMs themselves only see paravirtualized virtio-blk / virtio-net devices.