Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group


Verified Proof-Carrying Code



Project Description

Proof-Carrying Code (PCC) is a scheme for executing untrusted code safely. The code producer sends together with the binary a proof that the code satisfies a given safety policy on the target platform. The code receiver only executes the code if the proof is valid and fits the program. The test wether a proof fits a program usually involves a verification condition generator (vcg), which given a program returns a formula that implies safety, and a proof checker, which given a proof and a formula checks if the proof fits the formula.

One main goal of the project is to develop a fully formal foundation of a PCC system. This includes verified components of the trusted code base and soundness of the safety logic. The formalization will make explicit what properties soundness guarantees, and under which assumptions the trusted code base (mainly the vcg) works correctly. The formalization of the receiver side will be generic in safety logic, safety policy, and target machine.

On the code producer side we will analyse existing methods for static analysis of programs and extend them to generate proofs in a suitable safety logic. These proofs must show the correctness of the analysis. The safety policies and analyses we will investigate are arithmetic overflow and ressource constraints (in time and space).

This project is funded by the DFG.



(in alphabetical order)




Isabelle Theories

Note: These theories require the development version of Isabelle. They have been tested with the version from February 14th 2005, which can be downloaded below.

PCC Framework Defines a generic VCG and requirements that guarantee its soundness.

Instantiation Progr. Lang. Safety Logic Safety Policy
SALTypeSafety SAL (without procedures, pointers) shallow embedded HOL Type Safety
SALOverflowShallow SAL shallow embedded HOL Type Safety, No Overflows
SALTime SAL shallow embedded HOL Type Safety, No Overflows, Bounded Runtime
SALMemory SAL shallow embedded HOL Type Safety, No Overflows, Bounded Memory
SALOverflowDeep SAL deep embedded FOA with
HOL inference system
Type Safety, No Overflows
JinjaPCC Jinja Bytecode
(fragment of Java Bytecode)
deep embedded FOA with OO elements No Overflows



The theory files in the zip archives below are written for Isabelle 2005. Contains the Program Analyzer (required only for the Jinja Theories)
Unzip to directory ~/work/PA Contains all PCC Theories
Unzip to directory ~/work/PCC/


Martin Wildmoser Last modified: Wed Jan 25 12:37:48 MET 2006