Overview
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.
Features
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.
Flow
OTF service provider (PCH Producer)
The Producer receives the PSL formula from the Consumer, along with the task to implement a functionally equivalent FPGA module. The Producer thus first automatically generates an HDL description of the monitor, using automated PSL synthesis tools. The Producer then employs the well-known VTR (from Verilog-To-Routing) tool flow, together with a specialized tool flow for the FPGA overlay ZUMA, to synthesize the description into an implemented module, i.e., an overlay bitstream. The provider then re-extracts the logic function of that bitstream into a format suitable for logic reasoning, and constructs a proof premise for sequential functional equivalence by forming what is called a sequential miter function of the specification and implementation, yielding an induction problem on the circuit state, which can be proven afterwards. The Producer sends the resulting inductive invariant and the overlay bitstream back to the Consumer.
Thus the producer's flow consists of:
- Receiving a PSL description of a monitor
- Synthesizing that description first into HDL and the into an overlay configuration bitstream
- Formulating the sequential equivalence proof for description and implementation
- Conducting the proof
- Sending proof and bitstream back to the provider
Contact
If you have any questions regarding the PCH demonstrator, please contact the research staff from Subproject B4.