pccgen depicts the process of generating and using a binary. The process begins with the code consumer defining and publicizing a safety policy. This policy defines formally what is meant by ``safety'' and also specifies the interface between the consumer and any binary provided by the producer. Taking the policy into account, the code producer compiles (or assembles) and proves the safety of a source program, through a process which we call certification. This results in a binary that can be delivered to the code consumer. Upon receipt, the consumer validates the safety proof enclosed in the binary. Finally, if the proof is found to be valid, the code consumer can safely execute the native-code part of the binary.
: The subset of DEC Alpha assembly language.
The following subsections describe each of these pha-ses in more detail. The whole process is based on concepts from logic, semantics, and type theory, and so the rest of this section is necessarily somewhat technical, with most details beyond the scope of this paper. We will thus attempt to explain only the basic technicalities and key intuitions here. Those readers who would like more details on the underlying theory can find them in a separate technical report [16]. The impatient reader may want to skip ahead to pf where we show, for the case of network packet filters, that proof-carrying code surpasses previous approaches in both safety and performance.