The seL4 microkernel, the “world’s most highly assured OS”, has just been released as open source, which will help it evolve beyond its military use, says NICTA.
seL4 is a joint project between NICTA and General Dynamics C4 Systems, a US aerospace and defence company. It is released under the GNU General Public License, version 2 and includes all of the kernel's source code, the mathematical proofs, as well as other code and proofs for building highly secure systems.
seL4 is the most advanced of the L4 microkernels – a small, third generation microkernel with about 8,700 lines of C code.
It has full ‘functional correctness proof’, so the implementation (written in C) adheres to its specification. 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.
Functional programming language Haskell was used to develop a high-performance C-based implementation of seL4 for ARM processors.
Professor Gernot Heiser, software systems research group leader at NICTA, told Techworld Australia that working in the interests of a defence company means there has not been a lot of research and development into its application outside this area.
“[Defence] is pretty much what GD [General Dynamics] are mostly interested in, so they are less interested in other use cases, particularly when it’s really small initial products that you don’t know if they will turn into something really big,” he said.
“The military… are the most focused on security and safety, and also they are the ones who are used to pushing the limits of technology and constantly looking for better solutions, etc. But we want to not keep on being dependent on military projects.
“We convinced General Dynamics that it was the best thing for everyone to get it out there and make it widely accessible and really help it to get into as many products as possible and as quickly as possible. And in the end, that will even create business for GD.”
Medical devices and industrial automation are two areas where Heiser hopes development will kick off.
“You can kill someone [with a pacemaker] remotely without leaving a trace through cyber-crime. [Faults in] insulin pumps kill thousands of people in the US every year,” he said.
“Any large industrial processing plant contains lots of computer-driven things. At one extreme end there are mines that are being fully automated, with vehicles driving around autonomously, etc. Then there are industrial robots that build cars or whatever.
"In many cases, it is just things going wrong because the software is way too complex and a fault of a component that is not really critical can affect the operation of the critical component. seL4 gives you guaranteed isolation between the critical and less critical parts of the system.”
But drones are still an important application for the seL4. Last month, NICTA tested the seL4 on a drone where it could detect and deter cyber-attacks, and isolate different flight controls or components so if one is compromised the attack does not propagate to the other controls.
The project is being funded by US Defense Advanced Research Projects Agency (DARPA) – the agency that also funded Boston Dynamics, which Google acquired last year. NICTA is also working with Boeing, Galois, Rockwell Collins and University of Minnesota on the project.
The seL4 will be deployed in a commercial Boeing unmanned aerial vehicle by 2016. “We have a relatively simple system at the moment; it doesn’t have the full functionality. So we are protecting against certain classes of [hacks] for that one.”
Read: Autonomous systems considered the next big thing in defence technology.
NICTA and General Dynamics will continue to play a support role for the seL4 now that it is open source.
Also, whoever builds a project using the OS under the GNU GPLv2 license has to distribute it under the same open source license or a newer version. For anyone who wants to use it outside of the license terms, they can contact General Dynamics to get a commercial type license.
“If you compare it to Linux, for example, there’s no one you can [ask to] get a different license for Linux because the copyright and ownership is spread among thousands of people, so that possibility doesn’t exist in theory. In seL4’s case, because GD continues to own it, that possibility exists,” Heiser said.
When it comes to the libraries, specifications and example programs, Heiser said they are mostly released under a 2-clause BSD license, with plus tools under either BSD or GPL. "Some of the user-level examples incorporate third-party open-source software, which enforce licence conditions on our improvements."
Heiser could not name the companies that are interested in developing projects using the seL4, but said there’s a small Australian company keen to get involved, which NICTA may work with.
“We are willing and happy to get into commercial arrangements for helping people to actually build their products. And on the traditional engineering side, GD is also well placed for that.”