NICTA open sources seL4 secure OS

National ICT Australia today formally released the secure seL4 operating system as open source in order to spur an international uptake.

Gernot Heiser, NICTA.

NICTA has partnered with United States military technology manufacturer General Dynamics for the release. The company is considering using the operating system in unmanned aerial vehicles (UAVs) to make them resistant to hacking.

The operating system runs on both Intel x86 and ARM reduced instruction set architectures.

The micro-kernel based seL4 is designed to be immune to common attacks such as stack-smashing, code injection and return-oriented programming, NICTA said.

NICTA's Gernot Heiser claimed in the ARM-architecture version, seL4 was the first and only general purpose operating system kernel with mathematical proof that the binary adheres to its specifications.

He told iTnews the aim was to make seL4 more popular and widely used.

Some 300 people have already signed up for the seL4 mailing list, and Heiser said other forums will also be developed for support and user discussion as needed.

Heiser and his team hope seL4 will find its way into highly dependable applications that range from self-driving cars, avionics, medical implants as well as industrial control and automation systems.

The operating system and associated 200,000 lines of formal proof will be released under the GNU Public Licence version 2.0, Heiser said.

System libraries will be released under the more liberal BSD license, along with the tools for operating system.

seL4 was the result of work by 12 NICTA researchers and University of New South Wales PhD staff and students over five years. It comprises 7500 lines of C-code, NICTA said.