A syntactic approach to foundational proof-carrying code
- 25 June 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 89-100
- https://doi.org/10.1109/lics.2002.1029819
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.Keywords
This publication has 15 references indexed in Scilit:
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Nature ,2005
- A stratified semantics of general references embeddable in higher-order logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Foundational proof-carrying codePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A type system for certified binariesPublished by Association for Computing Machinery (ACM) ,2002
- A dependently typed assembly languagePublished by Association for Computing Machinery (ACM) ,2001
- The design and implementation of a certifying compilerPublished by Association for Computing Machinery (ACM) ,1998
- From system F to typed assembly languagePublished by Association for Computing Machinery (ACM) ,1998
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Safe kernel extensions without run-time checkingPublished by Association for Computing Machinery (ACM) ,1996
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994