sible. A proactive approach (such as
correctness-by-construction12) should
lower the cost significantly.
Second, building certified software
does not mean that programmers
must verify the correctness of every
component or algorithm used in its
code; for example, in micro-kernels or
virtual-machine monitors, it is often
possible for programmers to verify a
small set of components that in turn
perform run-time enforcement of
security properties on other components. 33
Dynamic validation (such as translation validation for compiler correctness26) also simplifies proofs
significantly; for example, it may be
extremely difficult to verify that a sophisticated algorithm A always takes
an input X and generates an output Y
such that R(X, Y) holds; instead, a programmer could extend A by adding an
additional validation phase, or vali-dator, that checks whether the input
X and the output Y indeed satisfy the
predicate R, assuming R is decidable.
If this check fails, the programmer
can invoke an easier-to-verify (though
probably less-efficient) version of the
algorithm A. To build certified software, all the programmer needs to do
is certify the correctness of the valida-tor and the easier version of the algorithm, with no need to verify algorithm
A anymore.
Third, the very idea that proofs and
specifications can be represented as
programs (within a computer) means
that developers should be able to exploit the synergy between engineering
proofs and writing large programs,
building a large number of tools and
proof infrastructures to make proof
construction much easier.
Finally, formal proofs for certified
software ought to be much simpler
and less sophisticated than those used
in formal mathematics. 11 Software developers often use rather elementary
proof methods to carry out informal
reasoning of their code. Proofs for software are more tedious but also more
amenable for automatic generation. 6, 28
Certified software also involves
other challenges. For example, time
to market is likely terrible, assuming
dependability is not a concern, so the
cost of certification would be justified
only if end users truly value a depend-
Since proofs are
incontrovertible
mathematical
truths, once
a software
component is
certified, its
trustworthiness
(with respect to
its specification)
would presumably
last for eternity.
ability guarantee. Deployment would
be difficult since most real-world engineers do not know how to write formal specifications, let alone proofs.
Pervasive certification requires fundamental changes to every phase in most
existing software-development practices, something few organizations are
able to undertake. The success of certified software critically relies on efforts
initially developed in the research
community.
Recent advances
Advances over the past few years in certified software have been powered by
advances in programming languages,
compilers, formal semantics, proof
assistants, and program verification.
Here, I sample a few of these efforts
and describe the remaining challenges for delivering certified software:
Proof-carrying code. Necula’s and
Lee’s 1996 work23 on proof-carrying
code (PCC) is the immediate precursor to the large body of more recent
work on certified software. PCC made
a compelling case for the importance
of having explicit witness, or formal
machine-checkable evidence, in such
applications as secure mobile code
and safe OS kernel extensions. PCC
allows a code producer to provide a
(compiled) program to a host, along
with a formal proof of safety. The host
specifies a safety policy and a set of
axioms for reasoning about safety; the
producer’s proof must be in terms of
these axioms.
PCC relies on the same formal
methods as program verification but
has the advantage that proving safety
properties is much easier than program correctness. The producer’s formal proof does not, in general, prove
the code produces a correct or meaningful result but does guarantee execution of the code satisfies the desirable
safety policy.
Checking proofs is an automated
process about as simple as program-ming-language type-checking; on the
other hand, finding proofs of theorems is, in general, intractable. Subsequent work on PCC focused on building a realistic certifying compiler4 that
automatically constructs proofs (for
simple type-safety properties) for a
large subset of Java and on reducing
the size of proof witness, an important