General Dynamics C4 Systems and Australia’s Information and Communications Technology Research Centre (NICTA) today open sourced the code-base of a secure microkernel project known as seL4. Touted as “the most trustworthy general purpose microkernel in the world,” seL4 has previously been adapted by organizations like DARPA as high-assurance systems used onboard military unmanned aerial vehicles and for similar defense and commercial uses.
NICTA, who formally verified seL4, and GDC4S, who owned it, are saying they have released the microkernel’s code-base so that anyone who wishes to build more dependable, safer, more secure and more reliable computer systems will have the capacity to do so. Therefore, not only are these organizations releasing seL4’s code, they are also making public its comprehensive formal verification, including “a complete proof chain from precise, formal statements of high-level security and safety properties to the binary executable code.”
And not only will anyone be able to build more secure and reliable systems, they’ll also be able to build these systems while spending less money per line of code, researchers say. This move could have huge implications in the sensitive fields of notoriously insecure critical infrastructure, increasingly connected automobiles and embedded medical devices, which have been proven remotely exploitable many times.
L4 microkernels are efficient, minimalist kernels that operate on the lowest level of a system in which only they execute in privileged mode. These microkernels function under the principle that larger systems are inherently buggier than smaller systems, particularly the kernels controlling these bigger systems. Thus, a smaller kernel minimizes a system’s susceptibility to kernel-targeting attacks that yield greater effect.
SeL4 is said to be “the world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement” and “the most advanced member of the L4 microkernel family.”
In addition to its small size, high performance, and policy freedom, all characteristics of earlier and lesser L4 microkernels, seL4 is said to have a built-in capability mode, which allows it to enforce security guarantees on the system and application levels.
NICTA notes that a secure system must be secure on all levels and that insecure systems are notoriously difficult to secure retroactively.
“seL4 provides the secure software base upon which further secure software layers (system and application services) can be composed to form a trustworthy embedded system,” the group wrote in an explanation of seL4. “The system could be as simple as an industrial controller needing isolation between two activities it manages, or as complex as virtualisation infrastructure requiring strong isolation between the virtual machines it provides to clients. Both scenarios rely on the guarantees provided by the underlying kernel.”
seL4 Microkernal Open Source
As outlined in their paper and in illustrated in the above graphic, “Leveraging separation kernels to create high assurance architectures with formally verified software components provides a means to implement such systems with measurable security enhancements.”
