Research breakthrough - Mathematically proving safety- and security-critical software

NICTA - August 12, 2009

NICTA today announced the completion of the world’s first formal machine-checked proof of a general-purpose operating system kernel, promising safety-critical software 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.

“It is hard to comment on this achievement without resorting to clichés,” says Professor of Computational Logic at Cambridge University’s Computer Laboratory, Lawrence C Paulson. “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,” explains NICTA Principal Researcher Dr Gerwin Klein, who leads NICTA’s formal verification research team.

Read entire story>>

Follow me on Twitter. Technological Singularity and Futurism is updated often; the easiest way to get your regular dose is by subscribing to our news feed. Stay on top of all our updates by subscribing now via RSS or Email.