A Syntactic Approach to Foundational Proof-Carrying Code (Extended Version)
Last modified: Tue Jul 5 20:57:46 2005 GMT.
AuthorsNadeem Abdul Hamid
AbstractProof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. In Foundational Proof-Carrying Code (FPCC), on the other hand, proofs are constructed and verified using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base.
Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and higher-order polymorphism. In this article, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker while the latter is known to be much easier to construct than the semantic soundness proofs. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system via an implementation in the Coq proof assistant.
PublishedJournal of Automated Reasoning (Special Issue on Proof-Carrying Code) 31 (3-4): 191-229, 2003.
Copyright © 1996-2022 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science