Linux Foundation backs security-oriented seL4 microkernel operating system

Want a truly secure operating system kernel? The Linux Foundation is partnering with Australia's national science agency, CSIRO, to roll out the seL4 microkernel.

First thing's first: Yes, the Linux Foundation is working with Data61 -- the digital specialist arm for Australia's national science agency, Commonwealth Scientific and Industrial Research Organisation (CSIRO) -- to push forward the new security-first operating system kernel seL4. But seL4 is not related to Linux. 

However, SeL4 can be used, in theory, as a foundation for Linux and other Unix related operating systems. For example, it was briefly considered for use in Richard M. Stallman's still-born Gnu Hurd operating system. Now, with its latest edition and broader support, seL4 may be more broadly deployed. 

This kernel is a member of the L4 microkernel family. SeL4 is a mathematically proven correct, bug-free operating system kernel. It's designed to enforce strong security properties. Data61 claims it's the world's first operating system with such proof. It's also, they say, the only proven operating system featuring fine-grained, capability-based security and high performance. In the real world, it supports mixed criticality real-time systems

The Linux Foundation's part in this is to host the newly formed seL4 Foundation. It "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, the Linux Foundation's VP of strategic programs. Founding members include Data61, UNSW Sydney, HENSOLDT Cyber GmbH, Ghost Locomotion, Cog Systems, and DornerWorks

SeL4 will be used in real-time embedded computing systems, which need the best possible security. It's expected to be used in such fields as avionics, autonomous vehicles, medical devices, critical infrastructure, and defense.  

In a statement, Carl L. Nerup, Cog Systems' Cog Systems' CEO, said:

"SeL4 has set the new standard for high assurance for embedded solutions on connected devices. This enables us to deliver commercial solutions that meet the rigorous demands associated with formal verification to deliver a certified  approach that meet the highest standard for safety and security in the market today."

Related Stories: