The Community for Technology Leaders
RSS Icon
Subscribe
Copenhagen, Denmark
July 22, 2002 to July 25, 2002
ISBN: 0-7695-1483-9
pp: 89
Nadeem A. Hamid , Yale University
Zhong Shao , Yale University
Valery Trifonov , Yale University
Stefan Monnier , Yale University
Zhaozhong Ni , Yale University
ABSTRACT
<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>
INDEX TERMS
null
CITATION
Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni, "A Syntactic Approach to Foundational Proof-Carrying Code", LICS, 2002, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science 2002, pp. 89, doi:10.1109/LICS.2002.1029819
46 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool