Programs from Proofs – A PCC Alternative

Abstract. Proof-carrying code approaches aim at safe execution of un-trusted code by having the code producer attach a safety proof to the code which the code consumer only has to validate. Depending on the type of safety property, proofs can however become quite large and their validation- though faster than their construction- still time consuming. In this paper we introduce a new concept for safe execution of un-trusted code. It keeps the idea of putting the time consuming part of proving on the side of the code producer, however, attaches no proofs to code anymore but instead uses the proof to transform the program into an equivalent but more efficiently verifiable program. Code consumers thus still do proving themselves, however, on a computationally inex-pensive level only. Experimental results show that the proof effort can be reduced by several orders of magnitude, both with respect to time and space.