Proof-Carrying Hardware: Runtime Formal Verification for Secure Dynamic Reconfiguration

This article proposes Proof-carrying Hardware (PCH) as a novel approach to bring formal verification to hardware security for reconfigurable platforms. The Proof-carrying Hardware combines a hardware module and a formal proof of safety which adheres to a previously established safety policy. These are produced by an untrusted external source and delivered in a unsecured way. The proof can then comparatively easily be verified by the reconfigurable platform, i.e., with a fraction of the effort that was required for computing the proof. The consumer can trust the module without any previous guarantees about any step of the production or the transmission.