Skip to main content


The jury is in: Monolithic OS design is flawed


Simon Biggs, Damon Lee and Gernot Heiser

UNSW Sydney



The security benefits of keeping a system’s trusted computing base (TCB) small has long been accepted as a truism, as has the use of internal protection boundaries for limiting the damage caused by exploits. Applied to the operating system, this argues for a small microkernel as the core of the TCB, with OS services separated into mutually-protected components (servers) – in contrast to “monolithic” designs such as Linux, Windows or MacOS. While intuitive, the benefits of the small TCB have not been quantified to date. 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.

BibTeX Entry

    publisher        = {ACM SIGOPS},
    doi              = {10.1145/3265723.3265733},
    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    author           = {Biggs, Simon and Lee, Damon and Heiser, Gernot},
    month            = aug,
    keywords         = {linux, microkernel, sel4, verification, exploit, operating system structure},
    year             = {2018},
    date             = {2018-8-27},
    title            = {The Jury Is In: Monolithic {OS} Design Is Flawed},
    address          = {Korea}


Served by Apache on Linux on seL4.