seL4 microkernel, the “world’s most highly assured OS”, is set to go open source on 29 July, 2014.
The project is run by NICTA and US-based company General Dynamics C4 Systems. NICTA said the OS is targeted for smartphones, cyber military systems, medical devices, and unmanned aerial vehicles or drones.
SeL4 is the most advanced of the L4 microkernels – a small, third generation microkernel with about 8,700 lines of C code.
A kernel is the software part of an operating system that runs in the privilege mode of a microprocessor. A microkernel is like a compact kernel that performs only minimal functions such as inter-process communication (IPC) with core functions such as file systems removed from the microkernel to run in user mode. Not having all functions run in privilege mode means that if one process breaks down, the other can still run efficiently.
seL4 has full ‘functional correctness proof’, so the implementation (written in C) adheres to its specification. Also, the binary code that executes on the hardware is a correct translation of the C code, meaning that the compiler does not have to be trusted and extends the functional correctness property to the binary.
This means the operating system is bug free and enforces integrity and confidentiality, NICTA said.
According to NICTA, secure operating systems such as KeyKOS and EROS, and the Cambridge CAP computer inspired the development of seL4. Functional programming language Haskell was used to develop a high-performance C programming language implementation of seL4 for ARM processors.
The release will include all of the kernel's source code, all the proofs, as well as other code and proofs for building highly secure systems.
Telsyte senior analyst Rodney Gedda said the OS system going open source means there’s opportunities for people to innovate and build upon it to make something bigger and better.
He added that NICTA could play a role in supporting the OS as it gains uptake.
“One of the best ways to increase uptake of an operating systems, even at a low level, is to release it free so that anyone can use it,” he said.
“And the business model around it is adding value to it. The same way Google released Android for free – it doesn’t make money on Android, but it makes money on top off it by selling content and services.
“So NICTA could be pursuing that approach with this operating system. It might not require licencing fees, but it might require support subscriptions. If they are going to be selling it to military device manufacturers or drone manufacturers, they are going to need continuous support. So even though it’s free, it will be sold with support contracts around it.”
Follow Rebecca Merrett on Twitter: @Rebecca_Merrett
Techworld has contacted NICTA and General Dynamics C4 Systems for comment.