In many application areas there is a rising need for high quality software. Proof-Carrying Code is a method that 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 (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, while these works mainly deal with type and memory safety properties, we are especially interested in PCC for classes of functional properties that are not restricted to only type and memory safeness.
Our research field about PCC is part of subproject B4 of the collaborative research center (CRC) 901 - "On-The-Fly Computing" of the DFG. Subproject B4 deals with “Proof-Carrying Services”. A service is a soft- or hardware component that can be assembled into dynamically – On-The-Fly – built service compositions. While building these service compositions it is inevitable to be able to prove the correctness of services very efficiently.
In our research group we are, among others, interested in the following research questions:
- For which types of properties is an automatic generation of efficiently verifiable proofs feasible?
- Is it possible to circumvent some theoretical limitations of proof-carrying code by combing PCC with monitoring?
- How could a PCC method for the compliance with protocols or call structures look like?
- How can PCC be used to guarantee the correctness of given pre- and postconditions inside of programs?
- How can PCC methods be combined with reachability analyses?