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技术可以通过提供一种允许对正式安全属性进行测试和测试和可信赖的可信赖计算机系统的设计来改变安全和可信赖的计算机系统的设计。经过验证。它可用于分析潜在的故障和漏洞的系统，以确保对设计限制的理解，既可以理解软件和硬件设计人员（通常没有正式的安全培训），并指导这些系统的重新设计以确保此类问题没有长期存在。这是一项允许工程师有效构建关键系统的能力技术，可以帮助保护用户和公众免受破坏事件的损害，并确保正式属性的概念受到练习计算机系统工程师的一阶设计约束。研究人员认为，我们的技术具有创造技能和工具的能力，即将嵌入的硬件和软件工程师需要评估其系统的可信度，并且可以减轻我们所有人都为了我们的安全和生计而依靠的关键系统的开发。