Secure embedded L4 (seL4), said to be the world’s most highly-assured operating system, has been released as open source, Australia’s Information and Communications Technology Research Centre of Excellence (NICTA) and U.S. aerospace and defense company General Dynamics C4 Systems announced on Tuesday.
The organizations are making available not only the source code for the seL4 microkernel, but also formal mathematical proofs, libraries, tools and programs that can be used as an example by those who want to develop secure systems.
“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.”
seL4, the most advanced member of the L4 microkernel family, is not susceptible to stack smashing, code injection or return-oriented programming (ROP) attacks because it’s designed not to operate in unspecified ways. According to NICTA, the operating system is bug free and it’s secure in the interpretation of classic operating system security.
The microkernel supports ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) and all modern x86 processor architectures, the organization noted in an FAQ.
At the beginning of July, NICTA published a video to demonstrate how seL4 could protect an aerial drone against cyberattacks. However, the organization points out that this is a general-purpose microkernel that’s ideal for embedded systems with security or reliability requirements, particularly on “platforms that provide virtual memory protection and for application areas that need isolation between different parts of the software.”
“seL4 takes software dependability to a new level, and will support the development of truly trustworthy systems,” explained Gernot Heiser, Software Systems Research Group Leader at NICTA. “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.”
seL4 code and proofs are available on GitHub under GNU General Public License, version 2.
A video demonstration from NICTA is embedded below: