seL4 Foundation’s mission to hard-code security into the OS

seL4 Foundation's mission to hard-code security into the OS

The CSIRO’s digital research and development arm, Data61, has announced the launch of the global seL4 Foundation, tasked with fast-tracking the development of systems based on the seL4 microkernel – an effort that could prove a massive leg-up for cybersecurity and operating systems developers.

Data61 hailed seL4 as the world’s first operating system (OS) kernel that is “mathematically proven to be secure”.

“This is the world’s fastest and most advanced OS microkernel,” the digital research agency said in a statement on the Foundation’s launch. “The kernel is the piece of software that runs at the core of any computer system and is responsible for ensuring overall security, safety, and reliability.”

As the “core” of all computer software functions, microkernels contain only the most basic code required to load operating systems and communicate with systems hardware.

The seL4 microkernel was uniquely developed to maintain isolation between trusted and untrusted components within a computer system, effectively enforcing security within componentised system architectures and allowing careful controls around software access to hardware devices within the system, Data61 noted in briefing documents.

seL4 itself contains only about 12,000 lines of C code, plus some assembly code. By comparison, a typical kernel, the foundation layer of an operating system, may contain upwards of 10 million lines of code.

The microkernel’s growing list of deployments range from defence systems to autonomous air and ground vehicles. Its ready adoption by defence agencies owes to trust in seL4’s capacity to better safeguard critical systems from security threats.

seL4 today stands as one of the key components of Data61’s research program. “We developed seL4 to provide a reliable, secure, fast and verified foundation for building trustworthy systems,” the digital research agency states on its website.

“This minimises the trusted computing base and has enabled us to verify seL4’s functional correctness and security properties using rigorous mathematical proof.

“The seL4-based systems have flown a helicopter and have handled classified military information. An earlier variant, OKL4, was deployed in over two billion phones.”

As a core piece of software, seL4 runs in Privileged Mode.

The newly launched seL4 Foundation will provide a global, independent, and neutral organisation for funding and steering the future evolution of seL4, Data 61 said in its launch statement.

Dr June Andronick, head of trustworthy systems at Data61 said the foundation will offer “a forum for developers and researchers to collaborate on growing and integrating the seL4 ecosystem, to maximise seL4’s benefits to critical systems across industry sectors around the world”.

“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,” Andronick said.

She added: ”seL4 is a game-changer for safety or security-critical systems; it forms a dependable base for building a trustworthy software stack”.

Among the international coterie to join the Foundation include a former program manager of the Washington-based Defense Advanced Research Projects Agency (better known as DARPA), Dr John Launchbury.

The DARPA-funded HACMS program has taken the lead in adopting seL4 on unmanned helicopters, demonstrating the microkernel’s protective credentials against security breaches.

Under future arrangements, the not-for-profit seL4 Foundation will team with the open-source Linux Foundation with slated plans to develop trustworthy operating systems based on the microkernel.

Simon Barry, Data61’s acting director, said the agency is proud to lead the creation of the seL4 Foundation.

“This is an example of the international impact that Data61’s research and development is creating.

“This enables safer, more secure and more reliable systems,” he said.

Locally, the seL4 Foundation will be chaired by Scientia Professor Gernot Heiser from the UNSW Sydney. He is joined by Dr Andronick together with Gerwin Klein, a chief principal research scientist at the CSIRO.

Representatives from two major international adopters of seL4 also join the forum: Sascha Kegreiss, chief technology officer of HENSOLDT Cyber, a Munich-based company that develops embedded IT products “that meet the highest security requirements”; and Dr Daniel Potts, the engineering director of Ghost Locomotion joins the group, whose California-based company develops self-driving cars using seL4.

Founding members of the seL4 Foundation are Data61, the UNSW Sydney, HENSOLDT Cyber GmbH, Ghost Locomotion Inc, Cog Systems Inc, and DornerWorks Ltd.

For more information on the seL4 development program, visit The seL4 Foundation.

seL4 is available as open-source software on the development platform GitHub.