4 ms·

Hypervisors are both older than microkernels and more secure. (The people who insist hypervisors are microkernels are ignorant of both technology and history.)

by msla 8y ago

wahern 8y ago
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...
snvzz 8y ago
>more secure. Hypervisors don't imply more secure. >(The people who insist hypervisors are microkernels are ignorant of both technology and history.) Truth. However, hypervisors implemented without microkernels won't be secure. Look at Xen and its large TCB for an example of doing it wrong. Look at seL4's VMM for an example of how it is done properly.

Hypervisors are both older than microkernels and more secure. (The people who insist hypervisors are microkernels are ignorant of both technology and history.)

by msla 8y ago

Hypervisors are both older than microkernels and more secure. (The people who insist hypervisors are microkernels are ignorant of both technology and history.)

wahern 8y ago

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

snvzz 8y ago

>more secure. Hypervisors don't imply more secure. >(The people who insist hypervisors are microkernels are ignorant of both technology and history.) Truth. However, hypervisors implemented without microkernels won't be secure. Look at Xen and its large TCB for an example of doing it wrong. Look at seL4's VMM for an example of how it is done properly.