World-first research breakthrough promises safety-critical software

The completion of the world’s first formal machine-checked proof of a general-purpose operating system kernel was announced by NICTA, Australia’s Information and Communications Technology (ICT) Research Centre of Excellence, paving the way for a new generation of software capable of unprecedented levels of reliability.

There is now a way to mathematically prove that the software governing critical safety and security systems in aircraft and motor vehicles is free of a large class of errors - long before the plane takes off or the car’s engine starts.

The Secure Embedded L4 (seL4) microkernel, designed for real-world use, has potential applications in defence and other safety and security industries where the flawless operation of complex embedded systems is of critical importance.

“We have a functional correctness proof which has never before been achieved for real-world, high-performance software of this complexity or size,” said NICTA Principal Researcher Dr Gerwin Klein, who leads NICTA’s formal verification research team. The proof also shows that many kinds of common attacks from hackers won’t work on the seL4 kernel.

The outcome is the result of four years’ research by Klein’s team of researchers and NICTA/UNSW PhD students - one of the largest machine-checked proofs ever performed.

NICTA will shortly transfer its intellectual property to its spin-out company Open Kernel Labs, whose embedded hyper-visor software - also based on NICTA research - is in hundreds of millions of consumer devices worldwide.

“The NICTA team has achieved a landmark result which will change the game for security- and safety-critical software,” said OK Labs’ Chief Technology Officer and Leader of NICTA’s ERTOS Group, Professor Gernot Heiser. “It provides conclusive evidence that bug-free software is possible; and in the future, nothing less should be considered acceptable where critical assets are at stake. OK Labs looks forward to taking this groundbreaking research to market.”