Mathematically-secure Australian seL4 microkernel gains global boost

Support of Linux Foundation will bring embedded-systems developers into military-strength secure ecosystem

teach train direct chalkboard math binary
Thinkstock

A new global foundation will help Australia’s government scientific research organisation dramatically expand the reach of a mathematically-verified secure operating-system kernel for applications such as autonomous vehicles, secure internet of things (IoT) devices, connected medical devices and military systems.

Designed to provide hack-proof embedded systems, the seL4 microkernel began life in 2009 as a research project of Australia’s Commonwealth Scientific and Industrial Research Organisation (CSIRO), which baked security into every aspect of the ultra-reliable, real-time environment.

Currently managed by the Trustworthy Systems team within CSIRO’s Data61 data group, seL4’s microkernel has been carefully defined and extensively tested using mathematical proofs that confirm it is highly reliable and impervious to compromise and attack.

Feted as a world first, these proofs have been maintained and tweaked by a dedicated verification team of around a dozen people — which work in lockstep with the development team to ensure that the microkernel cannot be compromised by outside actors.

Yet despite its successful use in hack-proof drones, autonomous vehicles, medical devices, IoT equipment and military applications “that we don’t really know about”, Scientia Professor Gerner Heiser told CSO Australia that taking the microkernel to the next level meant extending the project’s service development and integration well beyond CSIRO’s core team.

“We have the expertise and have to provide a lot of the components required to make the system usable and help people build with it,” he explained, “but this is just not scalable enough — so we have become a big bottleneck.”

The newly-launched seL4 Foundation has been designed to resolve this bottleneck by engaging with well-resourced industrial partners that want to integrate the real-time operating system into real-world devices where secure, ultra-reliable design is essential.

The Linux Foundation is a core partner of the new foundation, throwing its weight and extensive community behind an effort that vice president of strategic programs Michael Dolan said would “provide a neutral, mature and trustworthy framework to help advance an operating system that is readily deployable and optimized for security.”

Engagement with the Linux Foundation was a massive coup for the seL4 effort, Heiser said, because that effort had years of demonstrated success in fostering an ecosystem of innovation built around a common operating-system core.

Whereas Linux integrates core services with its kernel into an operating system, however, the seL4 approach will maintain the kernel in-house and allow outside parties to layer their own services and components on top.

“It’s easier to manage this way because you don’t break the kernel even if you break something in these user-land components,” Heiser explained. “You can provide a much higher degree of autonomy to developers, which should make it easier to see how the seL4 ecosystem can scale up.”

“A basic idea of the foundation is to bring these players to the table and let them pool funding to make it possible in ways that none of the individual companies could do.”

The foundation’s launch has been two years in the making, during which time the Data61 team was engaged selling the idea internally and externally, improving its documentation and support systems.

Separating the kernel from its implementation will allow the two dozen-strong Data61 team to maintain its focus on “big-ticket items” such as the almost-complete mathematical verification of a new 64-bit, multi-core seL4 kernel.

Such kernels “are big, multi-million dollar projects that are above the pain limits of the companies that want to make this happen,” Heiser said. “Nobody else has the insights into the kernel design or verification practicalities; it’s often difficult to judge the implications of any changes to the kernel on the verifications.”

By fostering worldwide innovation around a demonstrably secure systems architecture, Heiser believes the seL4 Foundation will provide a highly attractive option for IoT developers that continue to struggle with security vulnerabilities that have proved difficult to iron out of other architectures.

The December launch of the Australian government’s Draft Code of Practice for Securing the Internet of Things for Consumers offered some guidance for developers of such devices, but taking it to the next level will require the kind of concerted development focus that an ecosystem like the seL4 Foundation enables. “Within a year, we hope to have some big companies putting real money into the project,” Heiser said. “We understand what we can do for this effort, but we would like to have a few dozen active developers of various components for the system.”

Copyright © 2020 IDG Communications, Inc.

The 10 most powerful cybersecurity companies