A Syntactic Approach to Foundational Proof-Carrying Code
Last modified: Tue Jul 5 20:56:47 2005 GMT.
Authors
Nadeem Abdul HamidZhong Shao
Valery Trifonov
Stefan Monnier
Zhaozhong Ni
Abstract
Proof-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. 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. In this paper, we present a syntactic approach to FPCC that avoids the difficulties of previous work. 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. 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.
Published
In Proc. Seventeenth Annual IEEE Symposium on Logic In Computer Science (LICS'02), Copenhagen, Denmark, pages 89-100, July 2002. ©2002 IEEE.- Gzipped Postscript [125k]
- PDF [200k]
- Coq (v7.3) prototype code (tar.gz) [45k]
- Coq (v8.0) prototype code (tar.gz) [45k]
