Journal article
A Trustworthy Proof Checker
Journal of automated reasoning, Vol.31(3/4), pp.231-260
2003
DOI: 10.1023/B:JARS.0000021013.61329.58
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.
Details
- Title: Subtitle
- A Trustworthy Proof Checker
- Creators
- Andrew W. Appel - Princeton UniversityNeophytos Michael - Princeton UniversityAaron Stump - Washington University in St. LouisRoberto Virga - Princeton University
- Resource Type
- Journal article
- Publication Details
- Journal of automated reasoning, Vol.31(3/4), pp.231-260
- DOI
- 10.1023/B:JARS.0000021013.61329.58
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- Language
- English
- Date published
- 2003
- Academic Unit
- Computer Science
- Record Identifier
- 9984259419502771
Metrics
1 Record Views