Over­view

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.

Fea­tures

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 Pro­vider (PCH Con­sumer)

The Consumer can request a new pixelstream monitor from the OTF service provider at runtime, by sending an exact specification in PSL, for instance demanding a maximum intensity of the red channel of 50%:

assert always (tDataRed[7:0] <= 8'd127);

This PSL formula is then sent to the OTF service provider, who processes it using the provider tool flow and sends back a Proof-Carrying Bitstream (configuration bitstream) that implements the new monitor and proves sequential functional equivalence of the implementation to the original PSL specification. The consumer checks the proof and then instantiates the new monitor, if it is trustworthy.

The consumer’s flow thus encompasses:

  • Sending PSL description of new monitor to OTF service provider
  • Receiving implemented bitstream and sequential equivalence proof
  • Checking if proof is actually an inductive invariant that is a strengthening of the original miter (fail if not)
  • Reconfiguring the monitor with the new functionality

OTF ser­vice pro­vider (PCH Pro­du­cer)

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

Re­lated Tools

  • MBAC is used to synthesize the PSL formulae to the Verilog HDL
  • yosys is employed as front-end synthesis tool
  • VTR (from Verilog-to-Routing) tool flow (ABC, VPR) is used for back-end synthesis and technology mapping
  • ZUMA scripts are used to transform the synthesized design into an overlay configuration bitstream
  • ABC (slightly modified) is used to form the sequential miter function, perform the induction, obtain the inductive invariant, and validate it afterwards
  • ReconOS is used to run the hardware / software co-design

Con­tact

If you have any questions regarding the PCH demonstrator, please contact the research staff from Subproject B4.