Blog: Code Breakthrough Delivers Safer Computing

Code Breakthrough Delivers Safer Computing
University of New South Wales (09/25/09) Trute, Peter

Computer researchers at the University of New South Wales and NICTA say they have proven that an operating-system kernel was 100 percent free of bugs. The team verified the kernel known as the seL4 microkernel by mathematically proving the correctness of about 7,500 lines of computer code in a project taking an average of six people more than five years. "What we've shown is that it's possible to make the lowest level, the most critical, and in a way the most dangerous part of the system, provably fault free," says NICTA researcher Gernot Heiser. The research could potentially improve the security and reliability of critical systems used by the medical and airline industries as well as the military. "The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake," Heiser says.

View Full Article