A trustworthy proof checker. 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.
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Garnacho, Manuel; Périn, Michaël: Convincing proofs for program certification (2009)
- Bauer, Lujo; Garriss, Scott; McCune, Jonathan M.; Reiter, Michael K.; Rouse, Jason; Rutenbar, Peter: Device-enabled authorization in the grey system (2005)
- Klapper, Robert; Stump, Aaron: Validated proof-producing decision procedures (2005)
- Stump, Aaron; Besand, Ryan; Brodman, James C.; Hseu, Jonathan; Kinnersley, Bill: From rogue to microrogue. (2005)
- Appel, Andrew W.; Michael, Neophytos; Stump, Aaron; Virga, Roberto: A trustworthy proof checker (2003)
- Crary, Karl; Sarkar, Susmit: Foundational certified code in a metalogical framework. (2003)