Blog: Safer Software

Safer Software
The Engineer Online (08/12/09)

Researchers at Australia's Information and Communications Technology Research Centre of Excellence (NICTA) have developed the Secure Embedded L4 (seL4) microkernel, which they say is the world's first formal machine-checked proof of a general-purpose operating system kernel. The researchers say the seL4 microkernel provides the ability to mathematically prove that software governing critical safety and security systems in aircraft and motor vehicles is free of large class errors. The microkernel has potential applications in military, security, and other industries in which the flawless operation of complex embedded systems is critical. "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," says Cambridge University Computer Laboratory professor Lawrence Paulson. NICTA principle researcher Gerwin Klein says the researchers have created a general, functional correctness proof, which he says is unprecedented for real-world, high-performance software of such a large size and complexity. The NICTA team invented new techniques in formal machine-checked proofs, made advancements in the mathematical understanding of real-world programming languages, and developed new methodologies for rapid prototyping of operating system kernels. "The project has yielded not only a verified microkernel but a body of techniques that can be used to develop other verified software," Paulson says. The research will be presented at the 22nd ACM Symposium on Operating Systems Principles, which takes place Oct. 11-14 in Big Sky, Montana.

View Full Article