Logic in Computer Science (LICS 2002)

Paper: A Syntactic Approach to Foundational Proof-Carrying Code (at LICS 2002)

Authors: Nadeem A. Hamid Zhong Shao Valery Trifonov Stefan Monnier Zhaozhong Ni

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; they certify safety but only if there is no bug in the typing rules. Foundational Proof-Carrying Code (FPCC), on the other hand, constructs and verifies its proofs 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. Furthermore, none of them can be easily extended to support mutable fields and higher-order polymorphism. In this paper, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker while the latter is known to be much easier to construct than the semantic soundness proofs.

BibTeX

  @InProceedings{HamidShaoTrifonovMo-ASyntacticApproacht,
    author = 	 {Nadeem A. Hamid and Zhong Shao and Valery Trifonov and Stefan Monnier and Zhaozhong Ni},
    title = 	 {A Syntactic Approach to Foundational Proof-Carrying Code},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }