The concept of Proof-Carrying Code (PCC) and Hardware (PCH) is defined in a two-party contract work scenario, where a Consumer creates a functional specification along with corresponding properties (functional or non-functional) that the resulting binary should or should not exhibit. A Producer is then tasked with creating such a binary together with a proof of conformance to the desired properties, resulting in a Proof-Carrying Binary that is sent to the Consumer, who then validates the proof and can afterwards know beyond any doubt if the received binary is trustworthy or not. For further details please read the description of subproject B4.

In the case of the Proof-Carrying Hardware Demonstrator, the target platform is a reconfigurable hardware device, like an FPGA, or a system-on-chip that includes programmable logic, and the binaries are thus configuration bitstreams for such programmable logic. The Proof-Carrying Hardware Demonstrator is a collection of software tools, scripts and hardware modules that demonstrate the PCH tool flow and show the proof-carrying hardware service exchange between a provider and an OTF service provider.

The demonstrator consists of a video stream processing pipeline in reconfigurable hardware, which is based on a single, Linux-based reconfigurable system-on-chip. Video frames are grabbed from an attached USB webcam, sent from the Linux in the processing system (PS) to the programmable logic (PL) and then passed through an image processing pipeline which, at the end, displays the final frames on an attached HDMI display. Within the pipeline is a pixelstream monitoring and enforcement unit, which is capable of checking pre-defined properties of individual pixels or a group of them, and then enforcing their conformance to said property. In the demonstrator, the enforcement unit works by setting conflicting pixels to a safe state (i.e., to black), and the monitor itself can be synthesized on-the-fly from a user-defined formula given in the Property Specification Language (PSL). For the combination of this monitoring and enforcement unit, a proof by induction will also be generated on-the-fly, proving that the final bitstream actually contains an implementation that indeed is true to the PSL specification and generates a pixelstream which is guaranteed to never contain any illegal pixels. Since we cannot interpret the bitstreams of current FPGAs, since their vendors do not disclose the format, we employ a virtual FPGA overlay with an open bitstream format, so that we can easily obtain the netlist from a bitstream.

To this end, we have generated two interwoven flows, one for the Consumer and one for the Producer, which in combination show the feasibility and flexibility of this powerful PCH certified runtime-monitoring technique. Within the OTF context, PCH can be applied at several places, to ease the following descriptions we will use the interaction between a OTF provider, who combines single services into a larger service to fulfill a user request, and an OTF service provider, who provides one of the single services, as example.