The goal of subproject B4 of the collaborative research center (CRC) 901 - "On-The-Fly Computing" of the DFG is the development of Proof-Carrying Services. The scenario we consider consists of two roles: A service producer and a service consumer. Services in this context are soft- or hardware components that can be assembled into dynamically – On-The-Fly – built service compositions. Thereby, while building these service compositions it is inevitable to be able to prove the correctness of services very efficiently.

Participants: Heike Wehrheim, Felix Pauck

Former Participants: Manuel Töws, Tobias Isenberg, Marie-Christine Jakobs, Alexander Schremmer, Nils Timm, Daniel Wonisch

Cooperations: RG Bodden, RG Platzner

Official website.

In many application areas there is a rising need for high quality software. Proof-Carrying Code (PCC) is one method that can be applied in our Proof-Carrying Services scenario. PCC is capable of ensuring the correctness of foreign software with respect to certain correctness properties efficiently.

Basically, PCC consists of two steps. First, the software developer (code producer) has to generate a proof of the correctness of his product. This proof has to be verifiable and is attached to the shipped software program. Since the proof generation involves a complete formal analysis of the software program, this step is typically very expensive. Second, the user of the software product (code consumer) has to validate the proof. This has to be performed such that (1) illegal changes of the proof (the proof does not show the correctness properties) as well as (2) modifications of the program (the proof does not fit to the software program) can be discovered. Furthermore, the attached proof has to be designed such that its validation is much more efficient (in terms of runtime and space consumption) than its generation.

First results of PCC for assembler programs were already published 1997 by Necula and Lee. However, these works mainly deal with type and memory safety properties. In contrast, our PCC framework is not restricted to these two functional properties.
Furthermore, we developed an alternative to this framework that relies on program transformation - Program-from-Proofs (PfP). Instead of sending a certificate along with the program, the analysis result computed by the producer is used to transform the program into an equal one which can be analyzed with a more light-weight analysis. This also eliminates the burden of using one specific analysis tool on the consumer side. To improve further, we explored combinations of verification and testing as another approach.

In our research group we are, among others, currently interested in the following research questions:

• Can different PCC techniques or combinations of those be used to certify arbitrary programs?
• Is it possible to certify real-world, large-scale programs through hierarchical certification of all its components?
• For which types of (hyper-)properties is an automatic generation of efficiently verifiable proofs feasible?

This project is funded by the Deutsche Forschungsgemeinschaft DFG (SFB 901)

Publications of SFB 901 B4