Breakthrough software testing technology hailed by a Cambridge University expert as a tool able to deliver “currently unimaginable standards of reliability” to software has been unveiled by NICTA chief executive officer Dr David Skellern.

According to Dr Skellern, NICTA’s formal verification research team has completed the world’s first mathematical proof of a general purpose operating system kernel. The Secure Embedded L4 (seL4) microkernel is being initially targeted at applications in defence and safety-critical sectors.

In a release issued by NICTA, Lawrence Paulson, professor of computational logic at Cambridge University’s Computer Lab, noted that; “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.”

Dr Skellern explained that the kernel is the central component of most operating systems, managing key computer resources. “The mathematical proof is not done manually…rather the proofs are machine checked, but they use automatic theorem proving software. The proof means the 7,500 lines of C-code that make up the kernel has the exact behaviour that has been specified for it.

“The significance of this breakthrough lies in being able to give much stronger assurances about the operation of critical safety and security systems. It would be very reassuring to know this was the case if you were in a plane in mid air – it is not so easy to reboot a plane’s computer systems when something goes wrong,” said Dr Skellern.

Continued page 2