Isabelle, 'Generic Proof Assistant,' at Your Service
Can we humans be trusted to write enterprise operating systems? Or is the endeavor just too complex?OS Roundup: It's pretty much a given that just about any code written by humans is riddled with bugs. Isabelle is an app that aims to change this with tools that verify code using a logical calculus.
We've certainly been giving it a go for the past few decades, and the results are not pretty: You can be fairly certain that just about any code written by humans is riddled with bugs, and such is the complexity of the software we write that these bugs can often go undetected for years.
Last week, for example, a pair of Google researchniks, Tavis Ormandy and Julien Tinnes, found a bug that's been lurking in the Linux kernel for neary a decade. "It affects all 2.4 and 2.6 kernels since 2001 on all architectures," Tinnes announced on his blog.
Ideally what we humans need, then, are a bunch of infallible robots to check our work and make sure we don't make any coding mistakes when we write the enterprise operating systems on which so many of us depend.
We don't have such robots, but we do have Isabelle, a "generic proof assistant" application developed at the University of Cambridge and Technische Universität München and available to download free under the BSD licence. Isabelle allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.
Last week, researchers down-under announced they used Isabelle to complete the first formal machine-checked proof of a general-purpose OS kernel. The kernel in question is the secure embedded L4 (seL4) micro-kernel, which has been designed to govern critical safety and security systems in aircraft and motor vehicles.
According to Dr. Gerwin Klein, head of the team of researchers in Australia that carried out the work on seL4, what has been achieved is a general functional correctness proof. It also shows that the kernel is not susceptible to many common attacks, such as buffer overflows. Which is nice given that the OS is involved in aircraft safety.
The good news is Klein's work may to lead to more secure and reliable enterprise operating systems in the future. "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," noted Larry Paulson, Professor of Computational Logic at Cambridge University's Computer Laboratory and one of the scientists behind Isabelle. "The project has yielded not only a verified microkernel but also a body of techniques that can be used to develop other verified software," he added.
But don't hold your breath. The bad news is that verifying the 7,500 of C in seL4 took 12 people four years, and involved proving more than 10,000 intermediate theorems in more than 200,000 lines of formal proof which Isabelle was then used to check. Given that the Linux and Windows kernels have more than 5 million lines of code, and that they certainly can't be frozen for years at a time while intermediate theorems are formally proved, enterprise operating systems that are up to date, unimaginably reliable and free from buffer overflow vulnerabilities aren't going to happen any time soon.
Unless someone comes up with the code-checking robots, of course.
Paul Rubens is a journalist based in Marlow on Thames, England. He has been programming, tinkering and generally sitting in front of computer screens since his first encounter with a DEC PDP-11 in 1979.