We transferred the idea of Proof-carrying Code to reconfigurable hardware. Proof-carrying hardware cannot only verify functional properties of a hardware service but also non-functional hardware-related properties.
The functional properties can be verified by formulating test functions that use the primary inputs and outputs of the circuit to determine if the desired properties hold.
Our first approach transforms these test functions into an unsatisfiability problem (unSAT) over boolean formulas, which can in many relevant cases be solved quite efficiently using a modern SAT solver. The resolution proof of the unsatisfiability becomes the certificate. For our proof of concept, we use the property of functional equivalence between a circuit implementation and its original specification as a catch-all property, to implement prototypes for Proof-carrying Hardware. We used this approach in particular for combinatorial circuits and sequential circuits with a fixed number of cycles. Due to the closed nature of FPGA vendor’s tools, we cannot use the configurations of actual FPGAs directly. Hence, for demonstration purposes we started with configuration bitstreams for an abstract FPGA. To create real prototypes for PCH, we extended our approach to use virtual FPGA overlays on top of real FPGAs that we can program using open source tool flows compatible with PCH.
To speed up the validation of the resolution proof, we have investigated implementing the validation in hardware itself, which revealed that the hardware solution can be competitive despite potentially large proof sizes and highly irregular access patterns necessary for validation, if a special memory interface like Hybrid Memory Cube is available.
We have also looked into guaranteeing non-functional properties of hardware circuits using PCH, which include the physical aspects of the hardware device and the hardware service that is implemented on the reconfigurable device. Since many of these physical aspects are malleable when using our virtual overlays, or behave non-deterministically because of the dependence on the physical synthesis of the overlay in addition to the virtual synthesis, we have first developed a solution for the worst-case completion time of sequential run-to-completion circuits, as this abstracts the non-determinism away in the clock frequency used for the virtual circuit. We have successfully created certificates for the invariant adherence of a circuit to a given cycle limit.
Reconfigurable platforms can greatly benefit from the verification of such non-functional, possibly security-critical features. In Figure 2 below, we depict two FPGA chips with three IP cores, as another example which we are currently investigating. Without placement constraints, the cores are placed in a way that may overlap and allows the individual modules to share resources on the chip, which allows for unintended data leaks and malicious data manipulation. The placement and routing on the right is performed under constraints that physically isolate the individual modules and thereby protect the integrity and confidentiality of their data. With isolated IP cores, the FPGA chip can simultaneously run multiple IP cores with different trust levels without compromising the security of the platform or the data.