Researchers prove kernel is secure

[Brian Warkoczeski]

Researchers prove kernel is secure

by Tom Espiner

August 15, 2009

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

The researchers this week 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 organization, this week 
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.

For rest of the article, see:

http://news.cnet.com/8301-1009_3-10310255-83.html?tag=newsEditorsPicksArea.0