A semantic model of types and machine instructions for proof-carrying code

Proof-carrying code is a framework for proving the safety of machine-language programs with a machinecheckable proof. Such proofs have previously defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying code that will allow a code producer to choose a programming language, prove the type rules for that language as lemmas in higher-order logic, then use those lemmas to prove the safety of a particular program. We show how to handle traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existentials, and covariant recursive types. 1 Introduction When a host computer runs an untrusted program, the host may want some assurance that the program does no harm: does not access unauthorized resources, read private data, or overwrite valuable data. Proof-carrying code Nec97 is a technique for providing such assurances. With PCC, the host -- called the code consumer -- specifies a sa...