technical Perspective
Learning to Do
Program Verification
By K. Rustan M. Leino
Doi: 10.1145/1743546.1743573
When yoU DeCiDe to use a piece of software, how do you know it will do what
you need it to do or what it claims to
do? Will it even be safe to run? Will it
interfere with other software you already have?
As a software engineer developing
that piece of software, what can you do
to ensure the software will be ready in
time and will meet your quality standards?
A long-standing dream of ideal software development calls for the use
of program verification as part of the
answers to these questions. Program
verification is the process by which one
develops a mathematical proof that
shows the software satisfies its functional specification. This dream had
grown roots already by the 1970s.
Since then, and especially in the last
decade, the technology behind program
verification has become an important
part of software development practice.
At Microsoft alone, a number of symbolic execution techniques, including
abstract interpretation, counterexam-ple-guided predicate abstraction, and
satisfiability-modulo-theories solving,
are used routinely to enhance the testing of software, in some cases even
mathematically verifying the absence of
certain kinds of software defects.
But what we use today pales in comparison to the grand dreams of the
1970s. Why? Is it not possible to provide
rigorous proofs of modern software? Is
it too difficult to capture in functional
specifications the intended behavior
of software? Is full program verification only for small algorithms and toy
examples? Are hardcore programmers
and verification experts not able to find
common goals to work toward? Is it not
cost-effective to insist that every detail
of a piece of software is correct?
The following work by Gerwin Klein
et al. is a landmark in the further de-
velopment of applying functional-cor-
rectness verification in practice. The
authors have produced a machine-
checkable proof of correctness for the
microkernel of an operating system.
For a user of the operating system,
this verification provides a number of
significant benefits; for example, the
assurance that no hostile application
running under this operating system
can subvert the integrity of the ker-
nel through a buffer-overrun attack.
For the software engineers involved,
the verification brings the benefit of
a code analysis that far surpasses that
achieved by testing alone.
a project like seL4
verification is not
easy to pull off. in
short, it is a big bet.
i applaud the team
for undertaking it.
The authors are careful to list not only
positive implications of the verification,
but also the assumptions upon which
the verification rests. This is important,
for all verification is performed at some
level of abstraction. For example, verifying a program at the level of abstraction
provided by a programming language
does not say anything about hardware
failures. Verification is not an absolute;
what it seeks to do is offer detailed aid
for programmers at the level of abstraction at which they are working.
A project like the seL4 verification
is not easy to pull off. It takes a strong
vision, as well as a significant amount
of work, expertise, and persistence. In
short, it is a big bet. I applaud the team
for undertaking it, and congratulate
them on delivering. Any doubts as to the
technical feasibility of such a project
should by now have been removed.
The question about cost-effective-ness, however, remains. Some may
argue that the end result of the verification—a level of assurance that could
not have been obtained using more traditional methods—has already made
up for the effort expended. Others may
balk at the 20 person-years to complete
the proof or at the ratio of 200,000 lines
of proof script to 6,000 lines of eventual
C code. I would like to offer a different
perspective on these numbers. First,
they provide a benchmark against which
to compare future work. I would expect
that in another decade, a similar project will take less effort and will involve
a larger degree of automation. Second,
the effort has resulted not just in an impressive engineering achievement, but
also in an appreciable amount of scientific learning. It is through pioneering
and repeated efforts like this one that
we will learn how to apply full program
verification on a more regular basis.
K. Rustan M. Leino ( leino@microsoft.com) is a Principal
Researcher at Microsoft Research, Redmond, WA.
