A proof-carrying based framework for trusted microprocessor IP

We introduce a proof-carrying based framework for assessing the trustworthiness of third-party hardware Intellectual Property (IP), particularly geared toward microprocessor cores. This framework enables definition of and formal reasoning on security properties, which, in turn, are used to certify the genuineness and trustworthiness of the instruction set and, by extension, are used to prevent insertion of malicious functionality in the Hardware Description Language (HDL) code of an acquired microprocessor core. Security properties and trustworthiness proofs are derived based on a new formal hardware description language (formal-HDL), which is developed as part of the framework along with conversion rules to/from other HDLs to enable general applicability to IP cores independent of coding language. The proposed framework, along with the ability of a sample set of pertinent security properties to detect malicious IP modifications, is demonstrated on an 8051 microprocessor core.