seL4 developers launch open source foundation to enable safer, more secure computer systems

As software becomes ever more complex and intertwined, it is crucial to ensure that systems cannot be compromised by even the smallest of defects. The seL4 microkernel, developed by CSIRO’s Data61, is designed to prevent such compromise.

The seL4 Foundation will provide a global, independent and neutral source of funding to support the future of seL4 to provide to a wide range of computer systems the essential protection it enables.

The Foundation will also act as a forum for developers and researchers to collaborate on growing and integrating the seL4 ecosystem, helping to maximise seL4’s benefits to critical systems across industry sectors around the world.

| What is seL4?

seL4 is the world’s first operating system (OS) kernel that is mathematically proved to be secure, besides being the fastest and most advanced OS microkernel. It is freely available and open source, running on a variety of ARM, x86 and RISC-V platforms.

A kernel is a critical piece of software that runs at the core of any computer system, controlling how other components interact with each other and the outside world. Ultimately, it is responsible for ensuring overall security, safety and reliability.

The seL4 operating system kernel was first created more than 10 years ago as the foundation for building secure and reliable software. Its code has been formally verified to be fully secure, and it provides the most flexible configuration mechanisms to system designers.

“seL4 is a game changer for safety- or security-critical systems,” explains Dr June Andronick, Leader of Trustworthy Systems at CSIRO’s Data61. “It forms a dependable base for building a trustworthy software stack.”

seL4 has been used to build prototypes of aircraft controllers, desktop terminals and web services. Its growing list of deployments range from defence systems to autonomous air and ground vehicles, safeguarding them from cyber threats.

| How seL4 has been used

During DARPA’s High­‐Assurance Cyber Military Systems (HACMS) project, Data61’s Trustworthy Systems group demonstrated that seL4­based systems can be highly-resistant to cyberattacks.

The control systems employed by autonomous ground and air vehicles in the project were converted to using seL4 methodology, to protect the safety and security of critical control software from defects found in other operating system components.

In a 2017 live test, one of these systems safely flew and landed an autonomous helicopter, with a DARPA team of penetration-testing experts unable to hijack the flight control software, even though they were provided with complete access to less­‐critical components and the system’s full source code.

In the Cross Domain Desktop Compositor (CDDC) project, Data61 developed an seL4-based system that allowed users to interact with graphical programs from multiple computers running in different security domains, using only a single keyboard, mouse and computer screen.

This work enhanced existing desktop interfaces with strong security guarantees, while retaining a seamless experience for end-users, as the verification of seL4 includes a proof of information flow security that ensures sensitive data from one computer cannot be read by attackers who control the other devices.

SeL4 is one of the key technologies that enables AltoCryptTM Stick, a small USB device that allows

SeL4 enabled a design for AltoCryptTM Stick using lower cost, smaller and more efficient commercially available components rather than the manufacture of custom government-only silicon. For a country like Australia that does not have a manufacturing industry for high-tech electronic components, seL4 is a vital security enabler for Australian security product makers.

| The seL4 Foundation

The Foundation will bring together developers of the seL4 kernel, seL4-based components and frameworks, and of those adopting seL4 in real-world systems. It will focus on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raise funds to accelerate development, and ensure the clarity of verification claims.

Scientia Professor Gernot Heiser from UNSW Sydney and CSIRO’s Data61 noted that the original developers of seL4 will remain highly engaged in steering the direction of the technology.

“This is about taking the seL4 ecosystem to the next level. While broadening the community of contributors and adopters, at Trustworthy Systems we will continue to drive the kernel’s evolution and the research that ensures it will remain the world’s most advanced OS technology.”

Other founding members of the seL4 Foundation in addition to CSIRO’s Data61 are UNSW Sydney, HENSOLDT Cyber GmbH, Ghost Locomotion Inc, Cog Systems Inc, and DornerWorks Ltd.

“Cyber security is a core focus for Data61, and it’s fantastic to see our work further expanding its global relevance and reach,

SeL4’s expanding global relevance and reach demonstrates Australia’s international thought leader in cybersecurity says Dr Simon Barry, Acting Director at CSIRO’s Data61.

“We are proud to lead the creation of the seL4 Foundation to enable safer, more secure and more reliable systems and this is an example of the international impact that Data61’s research and development is creating.”

seL4’s 12,000 lines of C code are available on GitHub.