TWC: Small: Collaborative: Toward Trusted Third-Party Microprocessor Cores: A Proof Carrying Code Approach

第三方硬件知识产权（IP）是一种用硬件描述语言（HDL）编写的代码，广泛应用于现代集成电路中。现代电子产品通常包括75%的第三方硬件IP和25%的内部设计，以提供定制或盈利优势。第三方硬件IP在商业和军事应用中的广泛使用引起了对安全和可信度的担忧，特别是在当今全球化的市场中。恶意修改模块的HDL代码可能会引入漏洞，从而危及集成该模块的更大系统的安全性。那么，如何保护电子设备免受第三方硬件IP可能被篡改的威胁呢？为此，该项目正在开发一个框架，以促进可证明可靠的微处理器内核的获取。从软件携带证明代码（PCC）中提取概念，将与安全相关的属性编码在时序逻辑中，以概述可信操作的边界。在微处理器内核的情况下，这些安全属性确保微处理器指令集体系结构（ISA）不会引入恶意的体系结构状态更改，从而防止攻击者使用编程接口利用恶意引入的硬件修改。然后由供应商制作这些安全属性的正式证明并提供给消费者，消费者可以自动检查安全性属性的正确性并验证其遵从性。作为该项目的一部分，正在开发一个用于开发可证明可信的微处理器内核的生态系统，包括基础框架、库、软件工具和演示，以及可信集成电路和系统的教育模块。

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.