Researchers make breakthrough in reliable software
Researcher's at Australia's NICTA complete project on proving software reliability
Software researchers have completed a project which they believe will introduce a new era of reliability and safety in software systems.
The project, conducted at Australia's NICTA, Information and Communications Technology (ICT) Research Centre of Excellence, has completed the world's first formal machine-checked proof of a general-purpose operating system kernel, to demonstrate the potential for software with a guaranteed level of high reliability.
Researchers not only created a new OS kernel that they say is suitable for real-world use, but developed new techniques in machine checking of software which will have further benefits for software development and verfication.
Being able to mathematically prove that an OS is free of a large class of errors has major implications in areas such as security and safety, and in areas like automated control systems for vehicles.
NICTA Principal Researcher Dr Gerwin Klein, who leads NICTA's formal verification research team, and was in charge of the four-year project commented: "Formal proofs for specific properties have been conducted for smaller kernels, but what we have done is a general, functional correctness proof which has never before been achieved for real-world, high-performance software of this complexity or size."
The project created a microkernel suitable for real-world use, the Secure Embedded L4 (seL4) microkernel, which researchers say will offer both meaningful dependability guarantees along with complete resistance to a number of different types of attacks such as buffer overflows.
The intellectual property developed by the project will now be turned over to NICTA spin-off company Open Kernel Labs (OK Labs).
"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."
Other computer science experts around the world hailed the achievement. Lawrence C Paulson, Professor of Computational Logic at Cambridge University said that the achievement "should eventually lead to software that meets currently unimaginable standards of reliability", while Yale University's Professor of Computer Science Zhong Shao commented: "It makes a significant advance toward building fully verified system software with meaningful dependability guarantees."