For those of us in the business of devices, Gernot Heiser needs no introduction. But for the rest of you, here’s a summary:
Gernot’s primary occupation is leading research in Trustworthy Systems, aiming to make software systems truly trustworthy. He also teaches Advanced Operating Systems at UNSW, which also has its own prize for the best-performing student, the Advanced Operating Systems Alumni Prize.
In 2006 he founded Open Kernel Labs (OK Labs) for commercializing L4 microkernel technology developed in his research lab. He served as Chief Technology Officer from 2006–2010, and as a Director from 2006 until OK’s acquisition by General Dynamics in August 2012.
Gernot’s trailblazing work in the microkernel industry has led some of us around here to nickname him the “Godfather of Modularity,” and I had the privilege to catch up with him for a quick conversation.
Gernot, care to weigh in on the monolithic vs. modularity debate for device design?
Sure, that’s easy. The monolithic OS design model, used by Linux, Windows, macOS, is fundamentally and irreparably broken from the security standpoint.
Security is only achievable with a microkernel design, that minimizes the “trusted computing base” (TCB), i.e. the part of the system on which security depends. Ideally the microkernel is verified, mathematically proved correct, as in seL4. That is only feasible with a really small system. Systems like Linux have a TCB that is far too large and complex to get right, they are inherently full of security holes. Their use in security- or safety-critical applications is at best grossly negligent and should be considered professional malpractice. It must stop.
And you have some serious research to back this up. Tell us about it.
Absolutely. I recently performed an analysis of Linux vulnerabilities listed as critical – meaning it is easy to exploit and leads to full system compromise, including full access to sensitive data and full control over the system.
For each of those vulnerabilities we analyzed how it would be affected if the attack were performed against a feature-compatible, componentized OS. In other words, an application running on this OS should only be dependent on a minimum of services required to do its job, and no others.
We evaluated all Linux vulnerabilities that had been classified “critical”, a total of 112 vulnerabilities.
You have my attention – what was the result?
Well, for starters, only 5 compromises (4%) were not affected by OS structure.
29% were eliminated simply by implementing the OS as a componentized system on top of a microkernel! The example I like to give is if a Linux USB device driver is compromised, the attacker gains control over the whole system, because the driver runs with kernel privileges. In a well-designed microkernel-based system, only the driver process is compromised, but since our application does not require USB, it remains completely unaffected.
Wow. What else did you uncover?
A further 11% of the vulnerabilities are eliminated if the underlying microkernel is formally verified (proved correct), as we did with seL4. These are exploits against functionality, such as page-table management, that must be in the kernel, even if it’s a microkernel. A microkernel could be affected by such an attack, but in a verified kernel, such as seL4, the flaws which these attacks target are ruled out by the mathematical proofs.
So, taken with the previously mentioned 29%, we proved that 40% of the exploits would be completely eliminated by an OS designed based on seL4.
So, the case for modularity keeps building.
Definitely. We also found that another 17% of exploits are strongly mitigated. These are the kinds of attacks where a required component, such as NIC driver or network stack, is compromised, and as a result compromising the whole Linux system, while on the microkernel it might lead to the network service crashing without being able to compromise any data.
So if my math is correct, 57% of attacks are either completely eliminated or reduced to low severity?
That’s absolutely correct.
Gernot, thanks for your time and data as it relates to device vulnerability. Where can readers learn more about what you’re up to?
Thanks, Carl. People can find me at https://microkerneldude.wordpress.com/