Today, NICTA and General Dynamics C4 Systems are jointly offering the secure embedded L4 (seL4) microkernel and formal mathematical proofs as open-source software. seL4 is the world’s most highly-assured operating system (OS) and the first OS kernel with an end-to-end proof of implementation correctness and security enforcement.
This means that the kernel is designed not to operate in an unspecifed way provided the proof assumptions hold true, ruling out common attacks like stack smashing, code injection or return-oriented programming. It also means that the kernel can enforce strict isolation, allowing it to protect critical assets from interference by potentially compromised untrustworthy components.
Available from midday today, the seL4 open source release includes all of the kernel's source code, proofs and specifications, plus tools, libraries and example programs useful for building highly trustworthy systems. All are under standard open source licensing terms.
“seL4 takes software dependability to a new level, and will support the development of truly trustworthy systems,” said Gernot Heiser, Software Systems Research Group Leader at NICTA, and Scientia Professor and John Lions Chair, UNSW.
“There is ample evidence of the fundamental shortcomings of today’s critical software. By open-sourcing seL4 we hope to create a world-wide community of developers of dependable systems, in application areas ranging from national security to automotive, avionics, medical implants, industrial automation and BYOD in corporate environments.
“What is being released today is not only the breakthrough proofs NICTA achieved in 2009, but a whole host of advanced work built on top of that in the last five years”, said Dr Gerwin Klein, Senior Principal Researcher and Leader of Formal Verification at NICTA. “This includes new, stronger security proofs, verification of not only the C code, but the binary of the kernel, and a large amount of support and example code that will enable developers to get started quickly. With the proof released, you don’t have to trust that the kernel was developed correctly - you can check the evidence yourself.”
About seL4 – a unique operating-system kernel
seL4 delivers an unprecedented degree of assurance, achieved through formal verification, i.e. mathematical proof techniques. Specifically, the version for the ARM architecture is the first (and still only) general-purpose OS kernel with a full functional correctness proof – a mathematical proof that the implementation adheres to its specification.
There are proofs that seL4, if used properly, will enforce integrity and confidentiality – core properties for critical applications. These properties are proved to be enforced not just by a model of the kernel, but the actual binary.
seL4 is also the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. This means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations), a requirement for supporting time-critical applications.
For more information, and to gain access to the open source release of seL4, please visit: http://sel4.systems/.
“This is a remarkable achievement,” said Yale University’s Professor of Computer Science Zhong Shao at the time. “It makes a significant advance toward building fully verified system software with meaningful dependability guarantees.”