Skip to Content

Crash-Proof Code

Making critical software safer
Fail-safe: June Andronick uses mathematical analysis to create crash-proof software.Fail-safe: June Andronick uses mathematical analysis to create crash-proof software.
Fail-safe: June Andronick uses mathematical analysis to create crash-proof software.

When a computer controls critical systems in vehicles and medical devices, software bugs can be disastrous: “unnecessarily risky” programs could put lives in danger, says June Andronick, a researcher at NICTA, Australia’s national IT research center. As a result of one recently discovered software vulnerability, she notes by way of example, “a car could be controlled by an attack on its stereo system.” She is trying to reduce these risks by making the most important part of an operating system—the core, or kernel—in such a way that she can prove it will never crash.

The currently favored approach to creating reliable software is to test it under as many conditions as time and imagination allow. Andronick instead is adapting a technique known as formal verification, which microchip designers use to check their designs before making an integrated circuit: they create a mathematical representation of the chip’s subsystems that can be used to prove that the chip will behave as intended for all possible inputs. Until now, formal verification was considered impractical for large programs such as operating systems, because analyzing a representation of the program code would be too complicated. But in a computing and mathematical tour de force, Andronick and her colleagues, working in Gerwin Klein’s lab at NICTA, were able to formally verify the code that makes up most of the kernel of an operating system designed for processors often found embedded in smart phones, cars, and electronic devices such as portable medical equipment. Because this code is what ultimately passes software instructions from other parts of the system to hardware for execution, bulletproofing it has a major impact on the reliability of the entire system.

“The work is hugely significant,” says Lawrence Paulson, a computer science professor at the University of Cambridge. Beyond showing that there’s no bug in the kernel that could cause it to crash, he says, the verification guarantees that the kernel will perform, without error, every function it was programmed to perform.

The task was made a little easier by the choice to develop a so-called microkernel. Microkernels delegate as many functions as possible—such as handling input and output—to software modules outside the kernel. Consequently, they are relatively small—in this case, about 7,500 lines of C code and 600 lines of assembler. “That’s really small for a kernel, but really large for formal verification,” Andronick says. The analysis was targeted at the thousands of lines of C code; new software and mathematical tools had to be developed for the task. The kernel was released in February, and the team is working on another version designed for the popular line of x86 processor chips.

Andronick doesn’t expect that the technique will scale to much larger software, but she doesn’t think it has to. Using verified code in key subsystems would allow developers to make sure that bugs in less rigorously examined programs—such as those used to interface with a car stereo—can’t affect critical hardware. It could also prevent a computer from locking up if it encounters a problem. Andronick wants more software developers to embrace formal verification “in fields where safety and security really matter,” she says. “We show that it is possible.”

Keep Reading

Most Popular

open sourcing language models concept
open sourcing language models concept

Meta has built a massive new language AI—and it’s giving it away for free

Facebook’s parent company is inviting researchers to pore over and pick apart the flaws in its version of GPT-3

transplant surgery
transplant surgery

The gene-edited pig heart given to a dying patient was infected with a pig virus

The first transplant of a genetically-modified pig heart into a human may have ended prematurely because of a well-known—and avoidable—risk.

Muhammad bin Salman funds anti-aging research
Muhammad bin Salman funds anti-aging research

Saudi Arabia plans to spend $1 billion a year discovering treatments to slow aging

The oil kingdom fears that its population is aging at an accelerated rate and hopes to test drugs to reverse the problem. First up might be the diabetes drug metformin.

Yann LeCun
Yann LeCun

Yann LeCun has a bold new vision for the future of AI

One of the godfathers of deep learning pulls together old ideas to sketch out a fresh path for AI, but raises as many questions as he answers.

Stay connected

Illustration by Rose WongIllustration by Rose Wong

Get the latest updates from
MIT Technology Review

Discover special offers, top stories, upcoming events, and more.

Thank you for submitting your email!

Explore more newsletters

It looks like something went wrong.

We’re having trouble saving your preferences. Try refreshing this page and updating them one more time. If you continue to get this message, reach out to us at with a list of newsletters you’d like to receive.