[aurelien]

The point about security is that it seems to present the same failure as kvm is for Linux kernel. If the hypervisor is in the ring 0 you have the risk of VM escape from one to another or the host itself.

How do you mitigate that risk?

[snvzz]

In seL4's virtualization support, VM exceptions are turned into messages and handled by VMM, a task running in unprivileged mode.

VMM has no more capabilities than the VM itself, thus a VM escape would be, outside of academics, of no value.

Refer to pages 8 to 10 in the OP PDF.