I-Corps: Provable Hardware Design for Integrity and Security

I-Corps：可证明的硬件设计的完整性和安全性

• 批准号: 1339522
• 负责人: Ryan Kastner
• 金额: $ 5万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-05-01 至 2013-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1339522&HistoricalAwards=false
• 关键词: Corps; Provable; Hardware; Design; Integrity

Researchers have developed gate-level information flow tracking (GLIFT) technology that allows security analysis to be done on both hardware and software together. The GLIFT technology also allows security properties to be formalized as assertions that are verifiable at design time and allows properties such as non-interference to be proven formally for time-sensitive hardware/software systems. By providing the tools necessary to identify and control undesirable flows of information (such as those that might be injected by an adversary) at the level of hardware, the GLIFT technology captures some of the most insidious and difficult to anticipate security problems. Ultimately this makes it possible to more tightly integrate computing systems from different levels of security in a reliable manner, reducing replication (decreasing size and power), and making system-level evaluation cheaper and faster. Specifically, GLIFT technology provides the capacity of ensuring that a specified subset of inputs could never affect a specified subset of outputs.The GLIFT technology may transform the design of secure and trustworthy computer systems by providing a methodology that allows formal security properties to be tested and verified. It can be used to analyze systems for potential faults and vulnerabilities, as a way to ensure design constraints are understood both software and hardware designers (whom often have no formal security training), and to guide the redesign of those systems to insure such problems no longer exist. It is an enabling technology that allows engineers to efficiently build critical systems, that helps protects users and the general public from damaging events, and ensures that the notion of formal properties are treated a first-order design constraint by the practicing computer system engineers. Researchers believe our technology has the ability create the skills and tools that future embedded hardware and software engineers will need to evaluate the trustworthiness of their systems, and that it will ease the development of those critical systems that we all depend on for our safety and livelihood.

研究人员开发了门级信息流跟踪（GLIFT）技术，可以在硬件和软件上同时进行安全分析。 GLIFT 技术还允许将安全属性形式化为可在设计时验证的断言，并允许对时间敏感的硬件/软件系统正式证明非干扰等属性。通过提供必要的工具来识别和控制硬件级别的不良信息流（例如可能由对手注入的信息流），GLIFT 技术可以捕获一些最隐蔽且难以预测的安全问题。最终，这使得以可靠的方式更紧密地集成不同安全级别的计算系统成为可能，减少复制（减小尺寸和功耗），并使系统级评估更便宜、更快。具体来说，GLIFT 技术提供了确保指定的输入子集永远不会影响指定的输出子集的能力。GLIFT 技术可以通过提供允许测试和验证正式安全属性的方法来改变安全且值得信赖的计算机系统的设计。已验证。它可用于分析系统的潜在故障和漏洞，作为确保软件和硬件设计人员（他们通常没有接受过正式的安全培训）理解设计约束的一种方式，并指导这些系统的重新设计以确保此类问题不会出现。不再存在。它是一项使能技术，允许工程师有效地构建关键系统，帮助保护用户和公众免受破坏性事件的影响，并确保从业的计算机系统工程师将形式属性的概念视为一阶设计约束。研究人员相信，我们的技术有能力创造未来嵌入式硬件和软件工程师评估其系统可信度所需的技能和工具，并将简化我们安全和生计所依赖的关键系统的开发。