The inspiration for proof-carrying code comes from the realm of static type systems, especially as embodied by the language Standard ML (SML). In the formal definition of SML [14], a formal theorem guarantees the safety of any type-correct SML program, for a rigorously defined notion of safety. There are, of course, many other type-safe programming languages, for example Modula-3 [17] and Java [20], but the use of mathematical formalism sets SML apart from the these languages, and as a practical matter this rigor provides the basic conceptual and technical foundations that we need to create checkable proofs.
With type-safe languages like SML in mind, we can get an intuitive idea about
how proof-carrying code works. Consider a compiler for SML. Agent A writes
an SML program and compiles it to a native-code target program. If we then
throw away the source program, how can we later convince an agent B that the
target program is safe? (We are assuming that agent B does not trust agent
A.) One way to do this is to have the compiler prove that the target
code correctly corresponds to the source code.
Now, as it turns
out, in the type theory of SML, not only can such a proof be written out
formally, but in fact it can be written in a typed language with the property
that any well-typed proof is guaranteed to be valid.
Proof-carrying code is thus an application of ideas from programming-language theory, in this case used for defining notions of safety that are useful for operating systems, and flexible enough to accommodate both high-level and low-level languages. With the growth of interest in highly distributed computing, web computing, and extensible kernels, it seems clear to us that ideas from programming languages are destined to become increasingly critical for robust and good-performing systems.