Proof-Carrying Services

The vision of the Paderborn based cooperative research centre (CRC) 901, On-The-Fly Computing, is the nearly automatic configuration and execution of individualized IT services, which are constructed out of base services traded in world-wide available markets. In this talk, we first briefly overview the goal and the research challenges of the CRC 901 and outline its structure. Then we turn to proof-carrying services, our approach for guaranteeing service properties in the On-The-Fly Computing scenario. The approach builds on the original concept of proof-carrying code, where the producer of a service creates a proof showing that the service adheres to a desired property. The service together with the proof is then delivered to a consumer, that will only execute the service if the proof is both correct and actually about the desired property. On-The-Fly Computing requires us to establish trust in services at runtime and benefits from a main feature of the proof-carrying code concept, which is shifting the burden of creating a proof to the service producer at design time, while at runtime the consumer performs the relatively easy task of checking an existing proof. We extend the concept of proof-carrying code to reconfigurable hardware and show a tool flow to prove functional equivalence of a reconfigurable module with its specification. As a concrete example we detail our work on combined verification of software and hardware for processors with dynamic custom instruction set extensions. We present three variants for combining software and hardware analyses and report on experiments to compare their runtimes.