Amy Felty - A semantic model of types for proof-carrying code

Proof-carrying code ( PCC) provides a mechanism for insuring that a host, or code consumer, can safely run code delivered by a code producer. In our PCC system, the host specifies a safety policy as a set of inference rules in higher-order logic. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those inference rules that can be easily checked. One advantage of the PCC approach to code safety is that the trusted computing base is extremely small; it includes only the proof checker for verifying the proof of safety.

Information about a particular programming language or compiler, such as the type system, is essential in constructing proofs of safety. In previous work on PCC, this information was included as new inference rules added to the base logic. Consequently, a different type checker had to be implemented for each programming language, and even for each compiler. We present a universal type framework in which we model types via definitions from first principles and then prove the typing rules as lemmas. All definitions and lemmas used in a particular proof are included inside it, and thus no modification to the proof checker is required to check it. As a result, a code consumer can use the same checker to check proofs of safety for programs compiled from different source languages. We show how to model traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existential types, and covariant recursive types.