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

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,
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.1029819SEARCH