First thing's first: Yes, the Linux Foundation[1] is working with Data61[2] -- the digital specialist arm for Australia's national science agency, Commonwealth Scientific and Industrial Research Organisation (CSIRO)[3] -- to push forward the new security-first operating system kernel seL4[4]. 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[5]. Now, with its latest edition and broader support, seL4 may be more broadly deployed.
This kernel is a member of the L4 microkernel family.[6] 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[7].
The Linux Foundation's part in this is to host the newly formed seL4 Foundation[8]. 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[9], 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