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