program verification still involves
a vexing “last-mile problem.” Most
software-verification research concentrates on high-level models rather
than on actual programs—valuable for
finding bugs but leaving a big gap that
must be closed before meaningful dependability claims can be made about
actual software. Failure to reason
about actual code also has serious implications for maintainability; for example, it is difficult for programmers
to pinpoint the source and a fix when
a new bug is identified and ensure that
subsequent updates (to actual code)
will not break the code’s high-level
model.
Leading research on certified software aims to tackle all three. For example, concerning the lack of good metrics, a line is drawn between the actual
machine-executable software and the
surrounding physical environment
(such as hardware devices and human
operators). We can neither predict the
future of the physical world nor formally certify human behavior, but at
least under a well-defined, stable hardware platform (such as the x86 instruction set), the behavior of each machine
executable is a rigorous mathematical
entity. With a formal specification stating its desirable behavior, we can (at
least in theory) rigorously “certify” that
the machine executable behaves as expected. A good dependability metric is
then just the formal claim developers
make and certify about each program.
The long-term goal for research on
certified software is to turn code—
often a system’s weakest link—into its
most dependable component. The
formal specification given may not
precisely capture the behavior of the
physical environment, so the overall
system may still not function properly,
but at least when a problem occurs,
programmers and users alike are assured that the behavior of the software
is properly documented and rigorously enforced. The specifications for
functional correctness of individual
components may occasionally be too
large to be comprehensible, but many
systemwide safety, liveness, and security properties can be stated succinctly
and certified with full confidence.
To address the second and third
difficulties, software developers must
also certify the actual system-software
Software
dependability is
often confused with
the dependability
of the software’s
execution
environment, which
consists of not just
hardware devices
but also human
operators and the
physical world.
code. Most needed is a new “certified”
computing platform where programmers have firm control over the behavior of its system software stack, including bootloader, OS kernel, device
driver, hypervisor, and other runtime
services. Software consisting of mostly
certified components would be easier
to maintain, because the effects of updating a certified component would be
easier to track, and new bugs would
quickly be localized down to the noncertified modules.
Constructing large-scale certified
software systems is itself a challenge.
Still unknown is whether it can be
done at all and whether it can be a
practical technology for building truly
dependable software. In this article, I
explore this new field, describing several exciting recent advances and challenging open problems.
What it is
Certified software consists of a machine-executable program C plus a
rigorous formal proof P (checkable by
computer) that the software is free of
bugs with respect to a particular dependability claim S. Both the proof P
and the specification S are written using a general-purpose mathematical
logic, the same logic ordinary programmers use in reasoning every day. The
logic is also a programming language;
everything written in logic, including
proofs and specifications, can be developed using software tools (such as
proof assistants, automated theorem
provers, and certifying compilers).
Proofs can be checked automatically
for correctness—on a computer—by a
small program called a proof checker.
As long as the logic used by programmers is consistent, and the dependability specification describes what
end users want, programmers can be
sure the underlying software is free of
bugs with respect to the specification.
The work on certified software fits
well into the Verified Software Initia-
tive (VSI) proposed by Hoare and Mis-
ra14 but differs in several distinct ways
from traditional program-verification
systems:
First, certified software stresses use
of an expressive general-purpose met-
alogic and explicit machine-checkable
proofs to support modular reasoning
and scale program verification to han-