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

TWC：小型：协作：走向可信的第三方微处理器核心：携带代码的证明方法

• 批准号: 1318860
• 负责人: Yiorgos Makris
• 金额: $ 21.66万
• 依托单位: University of Texas at Dallas
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-10-01 至 2016-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1318860&HistoricalAwards=false
• 关键词: TWC; Small; Collaborative; Toward; Trusted

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.

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