Third-party hardware Intellectual Property (IP), written as code in a Hardware Description Language (HDL), is extensively used in modern integrated circuits. Contemporary electronics typically include 75% of third party hardware IP and only 25% in-house design to provide customization or a profit-making edge. Such extensive use of third-party hardware IP in both commercial and military applications raises security and trustworthiness concerns, especially in today's globalized market. Malicious modifications to a module's HDL code may introduce vulnerabilities, jeopardizing the security of the larger system within which it is integrated. So how does one protect electronics from the threat of potentially tampered with third-party hardware IP? To this end, this project is developing a framework for facilitating acquisition of provably trustworthy microprocessor cores. Drawing concepts from software proof-carrying code (PCC), security-related properties are codified in a temporal logic to outline the boundaries of trusted operation. In the case of microprocessor cores, these security properties ensure that the microprocessor instruction set architecture (ISA) does not introduce malicious architectural state changes, thereby preventing attackers from using a programming interface to exploit maliciously introduced hardware modifications. A formal proof of these security properties is then crafted by the vendor and presented to the consumer, who can automatically check correctness and validate compliance to the security properties. An ecosystem for developing provably trustworthy microprocessor cores, including a foundations framework, libraries, software tools, and demonstrations, as well as an educational module on Trusted Integrated Circuits and Systems are being developed as part of this project.
