Work Package 4 Proof Carrying Code

The overall objective of this work package is to develop a Proof Carrying Code (PCC) infrastructure that allows code consumers to formally check functional and security properties of code before executing it.

Goals:

• develop a long-term vision for applications of PCC in global computing
• define a certificate format that enables off-device and ondevice checking
• develop techniques to generate certificates from the results of both logical verification and type checking of both source and bytecode programs.

Scientific Objectives

Any successful Proof Carrying Code infrastructure must address the following three key aspects:

1. Proof development: How can code producers produce proofs of relevant program properties?
2. Certificate format: How can proofs be represented in a compact way such that proof checking can be done efficiently?
3. Proof checking: How can code consumers check proofs reliably and efficiently?

Applying PCC to security and functional properties of code requires significant progress in each of these areas leading to the following scientific objectives for this work package:

Proof development

Security and functional properties require powerful reasoning techniques. This work package will develop the foundations for the generation of PCC certificates from various analyses such as advanced type systems, logic-based techniques, and combinations of both. In particular, it will investigate a new form of compiler that can transform proofs from source to byte code level.

Certificate format

We will define a certificate format that can represent specifications and proofs of security and functional program properties. The scientific objective in this area is to investigate the trade-offs between certificate size and the resource requirements for proof checking. This research will lead to a certificate format that can represent proofs of complex security and functional properties.

Proof checking

Considering both on-device and off-device checking will allow a wide range of possibilities for the deployment of PCC. To do on-device checking requires minimizing its memory and CPU usage as well as its size and complexity. Off-device checking will allow a greater degree of proof complexity and functional verification but will require an infrastructure of replicated and distributed trusted proof checkers.

This work package will develop a long-term perspective and an infrastructure for the application of PCC in global computing. This infrastructure, modeled on the traditional PCC architecture, will address security and functional properties of code. In particular, it will consist of:

• certificate format
• certificate generator
• proof-transforming compiler
• off-device and on-device proof checkers.

Structure of the work package

Task 4.1 Scenarios for Proof Carrying Code

We will study possible scenarios for PCC in global computing, which may involve intermediaries, besides code producers and consumers. Moreover, the code being certified is not monolithic but rather made up of components from different sources.

Task 4.2 Certificates

We will develop a formal notion of certificate as a vehicle for PCC that can represent both the type-based analysis information of WP 2 and proofs in the byte code logic of WP 3. The size of certificates and costs of proof checking will be optimized to make on-device verification feasible.

Task 4.3 Generation of Certificates

We will study how to generate compact certificates from the output of type checking, logical reasoning, and program analysis. The results of this will lead to the implementation of a certificate generator.

Task 4.4 Proof-Transforming Compiler

We will develop a type-preserving compiler that transforms source-level proofs into the byte code logic. This compiler allows one to reason about source code by type-based and logicbased techniques, and to translate the outcomes to the byte code level.

Task 4.5 On-device Proof Checking

We will investigate how to implement the consumer part of the PCC technology on a constrained device. The main difficulty is to develop a proof checker that can operate within the memory and CPU usage constraints of, for example, a mobile device.

Role in the Project

The results of several earlier tasks are used directly within the tasks of this work package. In particular, the core program logic for byte code developed in Task 3.1 provides a foundation for the PCC infrastructure in Task 4.1 and for the PCC certificates designed in Task 4.2. In order to allow Proof Carrying Code to be deployed on interesting and realistic global computing applications, the work in Task 3.2 shows how to cover resource and information flow properties and the work in Task 3.3 shows how to deal with multi-threading. In order to deploy PCC certificates arising from typed based analysis, Tasks 2.3 and 2.4 will provide needed enhancements to type structures to deal with important low-level correctness and security features of code.