Published on *Computer Science Department at Princeton University* (http://www.cs.princeton.edu)

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.