A Trustworthy Proof Checker

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-TCB
checker, and we explain its design principles, and the representation
issues of the logic, safety predicate, and safety proofs. We show
that the trusted code 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.