The Community for Technology Leaders
Logic in Computer Science, Symposium on (2002)
Copenhagen, Denmark
July 22, 2002 to July 25, 2002
ISSN: 1043-6871
ISBN: 0-7695-1483-9
pp: 89
Nadeem A. Hamid , Yale University
Valery Trifonov , Yale University
Zhaozhong Ni , Yale University
Stefan Monnier , Yale University
Zhong Shao , Yale University
<p>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.</p> <p>Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building so-phisticated 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.</p>
Nadeem A. Hamid, Valery Trifonov, Zhaozhong Ni, Stefan Monnier, Zhong Shao, "A Syntactic Approach to Foundational Proof-Carrying Code", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 89, 2002, doi:10.1109/LICS.2002.1029819
114 ms
(Ver 3.1 (10032016))