Researchers prove kernel is secure

Australian researchers have demonstrated a way to prove core software for mission-critical systems is safe.

The researchers on Thursday said they can prove mathematically that code they have developed, designed to govern the safety and security of systems in aircraft and motor vehicles, is free of many classes of error.

Australia's Information and Communications Technology Centre of Excellence (Nicta), a private-sector research organisation, on Thursday announced the completion of the first formal machine-checked proof of a general-purpose operating-system kernel. The kernel is called the secure embedded L4 (seL4) microkernel.

Lawrence Paulson, professor of computational logic at Cambridge University's Computer Laboratory, who developed the Isabelle generic proof assistant Nicta modified to check its kernel, told ZDNet UK that the microkernel breakthrough would have a trickle-down effect for businesses.

"I regard the software industry as a real mess," Paulson said on Thursday. "If you've ever used a computer you know how unreliable they are. This is an important way of making it better."

While rigorously testing high-quality code is expensive, said Paulson, developing such tests and operating systems for specialised purposes would have the secondary effect of improving software in general.

Paulson added that teams in Europe had also made breakthroughs in the formal verification of computer systems, giving the German Verisoft project as an example.

Nicta principal researcher Gerwin Klein, who leads the formal verification research team, said in a statement that previous research had concentrated on giving proofs for specific system properties.

"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," said Klein.

Nicta claimed that many kinds of attack, such as those exploiting buffer-overflow vulnerabilities, would not be successful against the seL4 microkernel.

The intellectual property generated by the Nicta research will be handed over to Open Kernel Labs, a Nicta spin-off firm, for further development. The research took four years, and was conducted by 12 Nicta researchers, in conjunction with the University of New South Wales.