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

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

• 批准号: 1319105
• 负责人: Yier Jin
• 金额: $ 24.37万
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-10-01 至 2017-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319105&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) 中汲取概念，将安全相关属性编入时序逻辑中，以概述可信操作的边界。就微处理器内核而言，这些安全属性可确保微处理器指令集架构 (ISA) 不会引入恶意的架构状态更改，从而防止攻击者使用编程接口来利用恶意引入的硬件修改。然后，供应商制作这些安全属性的正式证明并提交给消费者，消费者可以自动检查正确性并验证对安全属性的合规性。作为该项目的一部分，正在开发一个用于开发可证明值得信赖的微处理器内核的生态系统，包括基础框架、库、软件工具和演示，以及可信集成电路和系统的教育模块。