Safer software

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.

All thanks to researchers at NICTA, Australia’s Information and Communications Technology (ICT) Research Centre 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 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,' said Prof 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.'