3 ms·
The main point remains: server and desktop OS kernels are a critical piece of infrastructure, worthy of full machine checked verification. In this context, it
by loup-vaillant 8y ago
The main point remains: server and desktop OS kernels are a critical piece of infrastructure, worthy of full machine checked verification.
In this context, it should be pretty obvious that a design that fails to minimise the trusted computing base is flawed. Even if a kernel vulnerability is unlikely to kill any given user, the sum of all the crashes, hacks, patching effort… is huge.
I bet my hat rewriting the entire kernel for all popular OSes would be far cheaper worldwide than not doing it. (Of course, this won't happen any time soon, because path dependence and network effects. Unless maybe someone works seriously on the 30 million lines problem described by Casey Muratory.)
> In other words, the ancient concept of "right tool for the job" still applies.
Absolutely. Monolithic kernels are clearly the wrong tool for the job.
- zokula 8y ago> Monolithic kernels are clearly the wrong tool for the job. Says who exactly?
- loup-vaillant 8y agoSays Simon Biggs, Damon Lee, and Gernot Heiser. Have you even read the abstract? > 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. If the effect is that huge, of course security trumps pretty much all other considerations. These are consumer OS kernels we're talking about. One that fails to more or less maximise security is obviously the wrong tool for the job. As the title of the paper suggests, in case you failed to read that as well.