Proof carrying-based information flow tracking for data secrecy protection and hardware trust

We discuss a new approach for protecting the secrecy of internal information in an Integrated Circuit (IC) from malicious hardware Trojan threats and, thereby, enhancing hardware trust. The proposed approach is based on Register Transfer Level (RTL) code certification within a formal logic environment. The key novelty lies in the introduction of a new semantic model for the Verilog Hardware Description Language (HDL) in the Coq theorem-proving platform, which facilitates tracking and proving secrecy labels of internal sensitive data and, by extension, security properties of the design. Additional framework enhancements include the ability to encapsulate sub-module properties in the top module proof environment, thereby strengthening the ability of Coq representation to reason on hierarchically organized RTL code. We demonstrate the proposed framework on a DES encryption core, wherein we employ it to prevent secret information (e.g. round keys) leaking by hardware Trojans inserted at the RTL description of the circuit.