Secure seL4 Microkernel Seeks to Build an Ecosystem Around New Foundation
The seL4 microkernel, the world’s first operating system kernel mathematically proven as “secure,” now has its own foundation, seL4 Foundation, which has been set up by the Linux Foundation along with Data61, the digital specialist arm for Australia’s Commonwealth Scientific and Industrial Research Organisation (CSIRO).
In essence, the seL4 microkernel is bug-free and mathematically proven to be secure, given certain assumptions around hardware and implementation. While the seL4 microkernel has been around since 2006, its adoption has yet to meet its full potential due to a lacking ecosystem.
“Over the last 10 years, seL4 started to take off and a number of organizations started to be interested, but what was really missing at this stage was an ecosystem around it,” said June Andronick, leader of trustworthy systems at Data61. “What I really look forward to is to lower the barrier for adoption for seL4, and really see that ecosystem growing in a way that people don’t hesitate to switch to seL4. We see a number of organizations that look for the best solution for the next product or the next generation of their product and they are driven to the direction of seL4, but they want to see the long term support. They want to see that there’s a community supporting it behind it.”
At the same time, explained Gernot Heiser, chair of the seL4 Foundation, the microkernel has seen adoption in a number of cases where security is of utmost importance. One example is a Boeing-built autonomous helicopter, which first used Linux and “took the official [penetration] testers about two weeks to completely own it.” Replacing Linux with the seL4 microkernel and then pulling out critical components into protected sandboxes with seL4 enforced isolation, said Heiser, proved to be impenetrable.
Compared to the Linux kernel, which Heiser said could “contain literally tens of thousands of bugs,” the seL4 microkernel is minute and essentially bug-free, coming in at just under 10,000 lines of code at its smallest, and 18,000 at its largest. The size varies according to the hardware on which it is running. Part of the reason seL4 can remain so small is that it leaves much of the work to the user, and Heiser explains that “an extreme viewpoint of what seL4 does is basically securely multiplexing hardware resources.”
Heiser also views this aspect of seL4 as an attractive quality from an open source perspective. While contributing to the Linux kernel can be difficult and requires following a very rigid process, contributing to the seL4 ecosystem is less restrictive, as that code is isolated and lives outside of the proven kernel itself.
“A lot of the functionality we have in a seL4-based system runs as user-level components. Like any application, and from the kernel’s point of view, there is no difference between a device driver, network stack, file system or an application — it’s just programs, and that is a great enabler for independent open source development,” said Heiser. “In seL4, because it’s an isolated user-level component, people can have a great degree of freedom of developing these things and contributing these things and we don’t need to keep such close control.”
Much like Windows and Linux, Heiser also explained that seL4 is written in C, but it differs in that it is a subset of C in order to keep the kernel provably secure.
“We had to stay away from some C features because C has ambiguous semantics. It’s not well-defined, so we had to restrict the language somewhat, but most of these restrictions were just common sense,” said Heiser. “A lot of the exploits you see in Windows and Linux are actually results of the insecurity of the C language — overflowing buffers and arrays, dereferencing uninitialized variables and null pointers are typical attack vectors. In principle, we have these things as well, but we prove explicitly that all these accesses are safe. We have proof that our kernel never dereferences a null pointer or never accesses an array out of bounds.”
The Linux Foundation is a sponsor of The New Stack.
