The Jury Is In: Monolithic OS Design Is Flawed
Microkernel-based Designs Improve Security
We address this by a study of critical Linux CVEs, where we examine whether they would be prevented or mitigated by a microkernel-based design. We find that almost all exploits are at least mitigated to less than critical severity, and 40% completely eliminated by an OS design based on a verified microkernel, such as seL4.
The Windows kernel, while not growing as quickly, is even bigger, with a recent version said to be 60-65 MSLOC (millions of source lines of code) [Ahmed 2016] compared to 26 MSLOC for Linux.
But even if we take the most optimistic estimate of 0.5/kSLOC, we can expect the Linux kernel to have about 13,000 bugs and the Windows kernel about 30,000.
The results are a stark confirmation of the arguments in favor of a small TCB. We find that 96% of critical Linux compromises would no longer be critical with a microkernel-based design, 40% would be completely eliminated by an OS based on a verified microkernel, and 29% even with an unverified microkernel.