It’s an email from your credit card provider, warning that your personal information has been left exposed to bad actors. It’s your city’s website and technical infrastructure locked up by ransomware. It’s control of a pacemaker being taken over by malicious hackers. It’s your safety being put at risk, and it’s the biggest motivator behind the efforts of those working to protect us from cyber threats.
One of those efforts is the seL4 microkernel, the world’s first operating system kernel with mathematical proof of its security. The seL4 microkernel was developed as an open source L4 microkernel by the Trustworthy Systems group in 2009, and experienced slow but steady adoption throughout the following decade. Now, thanks to CSIRO‘s Data61, under Australia’s national science agency, the seL4 Foundation has been established to expand the use and capabilities of trusted software based on this technology.
“seL4 is a game changer for safety- or security-critical systems; it forms a dependable base for building a trustworthy software stack,” said Dr June Andronick, Leader of Trustworthy Systems at CSIRO’s Data61. “We are taking this step to increase participation from the seL4 community, to aid further adoption and provide a sustainable, long-term trajectory for seL4. We are impressed with the strong support for this move from developers and adopters around the world.”
seL4 is a microkernel that provides the bare minimum of components needed to form an operating system. Microkernels are great for providing isolation (or separation) for improved functionality in the case of malfunctioning or crashing. The minimal number of components offer a heightened level of security.
seL4 in particular provides a high level of assurance without sacrificing performance – which is common paradigm system designers are often faced with. seL4 is unique because of its comprehensive formal verification, without compromising performance. It is meant to be used as a trustworthy foundation for building safety- and security-critical systems.
The seL4 Foundation exists under the greater Linux Foundation which will, “Support the seL4 Foundation and community by providing expertise and services to increase community engagement, contributors and adopters, helping to take the OS ecosystem to the next level.” said Michael Dolan, VP of strategic programs for the Linux Foundation. “The open governance and standards-based model will provide a neutral, mature, and trustworthy framework to help advance an operating system that is readily deployable and optimized for security.”
This independent nonprofit aims to provide ongoing technical leadership, responsiveness, and support for the seL4 community.
The main goals of the seL4 Foundation are the following:
Along with CSIRO’s Data61, launch members include DornerWorks Ltd., Cog Systems Inc, HENSOLDT Cyber GmbH, and UNSW Sydney, all also members of the Linux Foundation. The initial governing board consists of Scientia Professor Gernot Heiser from UNSW Sydney and CSIRO’s Data61; June Andronick; Gerwin Klein, Chief Principal Research Scientist, CSIRO’s Data61; and Dr. John Launchbury.
Launchbury presented a real-life demonstration of the seL4 microkernel’s security potential as program manager of the HACMS program, funded by DARPA. After a team of government-trained penetration testers took over the controls of a commercially available drone in a matter of minutes, they were stumped for hours before giving up on hacking into a drone running the seL4 OS.
Launch member DornerWorks Ltd. has ported seL4 to the Xilinx Zynq UltraScale+ MPSoC, proposed its use as a method of enhancing security for IoT products, and furthered its use in open source application on RISC-V architecture. Secure product development using the seL4 microkernel has become one of DornerWorks primary services since the company’s engineers first began contributing to the seL4 codebase.
“The seL4 proof provides a secure foundation to answer the growing need for cyber-security,” says DornerWorks vice president of marketing and sales Lance Hilbelink. “By joining the seL4 Foundation, DornerWorks can do more to help accelerate customer adoption of seL4 as the trusted software base for their embedded products. We’re looking forward to the future of seL4 kernel and tool development.”