Common hypervisors like ESX and Xen definitely aren't like microkernels, though they'd be more secure if they actually were. ESX and Xen are more like monolith

Common hypervisors like ESX and Xen definitely aren't like microkernels, though they'd be more secure if they actually were. ESX and Xen are more like monolithic kernels. The problem is that in practice they've become mini-kernels with their own driver systems and increasingly large code surfaces, recapitulating the mistake of monolithic kernels. seL4 actually can act as a hypervisor, and their build framework comes with support for building Linux guests into the bootable system image. I don't know if there are proofs of security wrt to the hypervisor, nor what the worth would be considering how complex the CPUs are these days, but I'd have much more trust in seL4 as a hypervisor and driver framework than in something using FreeBSD or Linux as the critical guarantor of system security. If you're stuck with commodity x86 or ARM hardware and really want a strong architecture, seL4 is the best option unless you want to build from scratch. Apple uses another L4 derivative as the OS for its security chips; an in-house derivative that predates the seL4 project.[1][2] [1] https://microkerneldude.wordpress.com/2016/04/14/so-the-fbi-cracked-the-iphone-with-a-zero-day-and-hardware/ https://microkerneldude.wordpress.com/2016/04/14/so-the-fbi-... [2] https://www.blackhat.com/docs/us-16/materials/us-16-Mandt-Demystifying-The-Secure-Enclave-Processor.pdf https://www.blackhat.com/docs/us-16/materials/us-16-Mandt-De...