PROBLEM: To test the reliability of software that controls embedded chips in medical devices and vehicles, computer scientists have relied on trial-and-error methods that can miss bugs.

SOLUTION: By using mathematical analysis to prove that a piece of software is reliable, June Andronick can take into account all possible inputs to the software, and all the possible ways the software could process those inputs.

Working at Australia's national IT research center (NICTA), Andronick and colleagues in Gerwin Klein's lab were able to use this analytical technique to write a small operating system that will always behave exactly as intended, never crashing (barring incorrect assumptions about the hardware).

Because the OS acts as the gatekeeper to the hardware, it can block instructions that would cause a crash—say, instructions coming from the application software that makes decisions about how an engine should be throttled. Some computer scientists predict that mathematically verifying the reliability of critical software components will become the norm in certain systems.

The technology could also help protect against cyber-attacks, Andronick says. The operating system could block unauthorized actions that are issued by software that has been hacked through some point of vulnerability, such as a Web browser. "The attack on the untrusted part can't keep the trusted part from functioning correctly," she says. —William M. Bulkeley