On 10 Aug 2020, at 07:03, Radev, Martin <martin.radev@tum.demailto:martin.radev@tum.de> wrote:
I am currently examining the possibility of using seL4 in a VM and writing a virtio driver to communicate with a virtio pci device in the HV.
I’ll let our engineers answer your question, but I have one of my own: What’s the point?
Running a verified seL4 kernel on an unverified hypervisor provides no benefits and loses all assurance. You might as well run Linux.
Gernot