A Trustworthy Proof Checker

Andrew W. Appel, Neophytos Michael, Aaron Stump, Roberto Virga

Research output: Contribution to journalArticlepeer-review

22 Scopus citations

Abstract

Proof-carrying code (PCC) and other applications in computer security require machine-checkable proofs of properties of machine-language programs. The main advantage of the PCC approach is that the amount of code that must be explicitly trusted is very small: it consists of the logic in which predicates and proofs are expressed, the safety predicate, and the proof checker. We have built a minimal proof checker, and we explain its design principles and the representation issues of the logic, safety predicate, and safety proofs. We show that the trusted computing base (TCB) in such a system can indeed be very small. In our current system the TCB is less than 2,700 lines of code (an order of magnitude smaller even than other PCC systems), which adds to our confidence of its correctness.

Original languageEnglish (US)
Pages (from-to)231-260
Number of pages30
JournalJournal of Automated Reasoning
Volume31
Issue number3-4
DOIs
StatePublished - 2003

All Science Journal Classification (ASJC) codes

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Keywords

  • Proof checker
  • Proof-carrying code

Fingerprint

Dive into the research topics of 'A Trustworthy Proof Checker'. Together they form a unique fingerprint.

Cite this