Making software safer

There is now a way mathematically to 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. All thanks to researchers at NICTA, Australia’s Information and Communications Technology (ICT) Research Center of Excellence, who have completed the world’s first formal machine-checked proof of a general-purpose operating system kernel.

The Secure Embedded L4 (seL4) microkernel itself, which has been designed for real-world use, has potential applications in defense and other safety and security industries where the flawless operation of complex embedded systems is of critical importance. “It is hard to comment on this achievement without resorting to clichés,” said Professor Lawrence Paulson at Cambridge University’s Computer Laboratory. “Proving the correctness of 7,500 lines of C code in an operating system’s kernel is a unique achievement, which should eventually lead to software that meets currently unimaginable standards of reliability.”

“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,” explained NICTA principal researcher Dr. Gerwin Klein, who leads NICTA’s formal verification research team.

The proof also shows that many kinds of common attacks will not work on the seL4 kernel. For instance, the microkernel is impervious to buffer overflows, a common form of software attack where hackers take control of programs by injecting malicious code. “Our seL4 kernel cannot be subverted by this kind of attack,” said Klein.

The outcome is the result of four years’ research by Klein’s team of twelve NICTA researchers, NICTA/UNSW PhD students and UNSW contributed staff. They successfully verified the C code and proved more than 10,000 intermediate theorems in more than 200,000 lines of formal proof. The proof is machine checked using the interactive theorem-proving program Isabelle. It is one of the largest machine-checked proofs ever done.

To reach this milestone, the NICTA team invented new techniques in formal machine-checked proofs, made advances in the mathematical understanding of real-world programming languages and developed new methodologies for rapid prototyping of operating system kernels. “This work goes beyond the usual checks for the absence of certain specific errors,” Paulson said. “Instead, it verifies full compliance with the system specification. The project has yielded not only a verified microkernel but a body of techniques that can be used to develop other verified software.”

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

A scientific paper describing this research will appear in the 22nd ACM Symposium on Operating Systems Principles (SOSP) here. Further details about NICTA’s L4 verified research project can be found here.