ing tools to manual proofs written by
hand and checked by a proof assistant
(a program that checks the correctness of proofs in expressive logic).
Preventing Software Hacks
Generally, computer code is written
without any formal processes, and the
main metric for testing it is simply trying
it out and seeing whether it or not works.
Testing does not necessarily guarantee all the bases have been covered that
might occur at runtime, or that it would
prevent a malicious attacker who reads
the program from devising something
clever with which to undermine it. Formal software verification relies on mathematical theorems and reasoning and
uses deductive techniques to check the
most critical aspects of a system. Proponents say this technique is making
hacker-proof software possible.
“A lot of the ways attackers take
over programs on machines and the
Internet is by exploiting security vul-nerabilities, and there are many kinds,
such as the buffer overrun vulnerability, to which safe languages are just immune,” notes Andrew Appel, professor
of computer science at Princeton University, who is considered an expert in
the program verification field.
Formal software verification uses
methods that don’t rely on running the
program; rather, they analyze program
text to prove things about its behavior
This is made possible by a process
known as software verification, and
verifying implementations of critical
systems like that radiotherapy setup is
one of the things about which Zachary
Tatlock is passionate. Over three years
ago, Tatlock was a Ph.D. candidate giv-
ing a talk at the university on his thesis
research in program verification. The
lead engineer for the medical center’s
radiotherapy team was in the audience,
and asked Tatlock how they could apply
verification to that system. “That prob-
ably helped me get hired,” Tatlock re-
calls. Today, he’s an assistant professor
of computer science at the university
and, with other colleagues and students
at UW, has also been working with the
team at the medical center ever since.
What makes the software verifica-
tion process challenging in the case
of the radiotherapy system described
here is that it is written in a variety of
languages, so different techniques
have to be deployed to verify the soft-
ware in its entirety. The system has
about a dozen components, each with
different levels of criticality.
Software for logging an event, for
example, is not as critical as software that verifies the beam power has
not become too high, Tatlock notes.
“What we want to be able to do is ensure the reliability of all pieces,” he
says. “We want to make sure there are
no bugs that can affect the parts that
are critical.” There are two or three
components “where the rubber meets
the road, and it’s super-critical to get
them right,” he says.
The radiotherapy system team uses
powerful verification methods ranging from automated theorem prov-
Software verification helps find the faults, preventing hacks.
Science | DOI: 10.1145/3105423 Esther Shein