I think this is a nice project but i wonder what exactly is verified vs. verifiable concerning the hosted linux kernels. its great if the HV is verified but verifiable and linux kernel in some VM are hard to combine in a sentence for many ppl.
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.
2 comments
[ 890 ms ] story [ 53.3 ms ] threadAlso 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.