Sciweavers

Share
LICS
2002
IEEE

A Syntactic Approach to Foundational Proof-Carrying Code

8 years 11 months ago
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...
Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, S
Added 15 Jul 2010
Updated 15 Jul 2010
Type Conference
Year 2002
Where LICS
Authors Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni
Comments (0)
books