Achtung:

Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Info-Icon Diese Seite ist nur in Englisch verfügbar
Bildinformationen anzeigen

Simplification of program analysis via certificates (PCC techniques) and program transformation

Proof-Carrying Code

Proof-Carrying Code (PCC) is a method that allows ensuring the correctness of software from external sources. The basic idea of PCC thereby is that software developers generate verifiable proofs of the correctness of their software and supply these with their software product. Users of the software can then, using these proofs, validate that the software is indeed correct. Essential for the technique is that this validation of the proof is much more efficient (in terms of runtime and space consumption) than the proof generation.

Participants: Marie-Christine Jakobs, Manuel Töws

Former Participants: Alexander SchremmerNils Timm, Daniel Wonisch, Tobias Isenberg

Cooperation: RG Platzner

Official website.

Description

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?

Funding

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

Ansprechpartner

Prof. Dr. Heike Wehrheim

Sonderforschungsbereich 901

Heike Wehrheim

Dr. Marie-Christine Jakobs

Spezifikation und Modellierung von Softwaresystemen

Marie-Christine Jakobs
Telefon:
+49 5251 60-1767
Fax:
+49 5251 60-3993
Büro:
O4.128
Web:

Manuel Töws

Spezifikation und Modellierung von Softwaresystemen

Manuel Töws
Telefon:
+49 5251 60-4272
Fax:
+49 5251 60-3993
Büro:
O4.137
Web:

Die Universität der Informationsgesellschaft