A Syntactic Approach to Foundational Proof-Carrying Code

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 ProofCarrying 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 la...

• Type: Conference
• Year: 2002
• Where: LICS
• Authors: Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
• Keywords: Automated Reasoning, Foundational Proof, FPCC, LICS 2002, Type System