Search
next up previous
Next: Esfandiar Haghverdi - Linear Up: Applied Logic / Logique Previous: Josee Desharnais - A

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



AMY FELTY, Bell Laboratories, Lucent Technologies, Murray Hill, New Jersey  07974, USA
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.


next up previous
Next: Esfandiar Haghverdi - Linear Up: Applied Logic / Logique Previous: Josee Desharnais - A