You know him SeL4 microkernel; THE Linux Foundation works with Data61, a digitally specialized division of the Australian National Science Agency, the Commonwealth Office for Scientific and Industrial Research (CSIRO), to promote the new core of the operating system seL4. But the seL4 not related to Linux.
For example, it is being used in Gnu Hurd's operating system Richard M. Stallman. Now, with the latest version and wider support, the seL4 can be developed more widely. But let's look at more details about the kernel designed for security.
This nucleus is a member of the family L4 microkernel.
The SeL4 is a mathematically proven error-free operating system kernel. It is designed to impose strong security features.
Data61 claims to be the first operating system in the world to be mathematically proven, and the only operating system to have proven security capabilities and very high performance. It will support very critical real-time systems in the future.
"He will support the foundation and its community SeL4 providing know-how and services to increase the involvement of the community, contributors and all those who adopt the system, helping the operating system environment to take it to the next level, ”said Michael Dolan,
Founding members include Data61, UNSW Sydney, HENSOLDT Cyber GmbH, Ghost Locomotion, Cog Systems and DornerWorks.
The SeL4 will be used in critical real-time computer systems where the greatest possible security is needed. It is expected to be used in areas such as avionics, autonomous vehicles, medical devices, critical infrastructure and of course defense.
In a statement, Carl L. Nerup, CEO of Cog Systems, said:
"The SeL4 has set a new high-reliability standard for built-in solutions on connected devices. It enables us to offer commercial solutions that meet the stringent requirements associated with formal verification to provide a certified approach that meets the highest standards of security and protection on the market today. ”