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.

People

(in alphabetical order)

Publications

Bytecode Analysis for Proof Carrying Code
Martin Wildmoser, Amine Chaieb, Tobias Nipkow; Proceedings of the First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005); Electronic Notes in Computer Science (ENTCS) [bibtex]
Asserting Bytecode Safety
Martin Wildmoser, Tobias Nipkow; Proceedings of the 15th European Symposium on Programming (ESOP 2005); (c) Springer-Verlag [bibtex]
Certifying Machine Code Safety: Shallow versus Deep Embedding
Martin Wildmoser, Tobias Nipkow; Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics 2004; (c) Springer-Verlag; 16 pages [bibtex]
Prototyping Proof Carrying Code
Wildmoser M.,Nipkow T.,Klein G.,Nanz S.; Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science 2004 [bibtex]

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

Download

The theory files in the zip archives below are written for Isabelle 2005.

PA.zip	Contains the Program Analyzer (required only for the Jinja Theories) Unzip to directory ~/work/PA
PCCTheories.zip	Contains all PCC Theories Unzip to directory ~/work/PCC/

Martin Wildmoser

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