NICTA tool revolutionises software reliability

Beverley Head
Wednesday, 12 August 2009 12:52

Business IT - Security

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.

Speaking at the opening of the 2009 NICTA Techfest in Sydney, which showcased 30 research projects underway at the national ICT research group, Dr Skellern said researchers last week completed the world’s first formal machine-checked proof of a general purpose operating system. In short the technology is a way for developers to test that the software they have designed works the way it is expected to, before it is put into production.

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