I-Corps: Provable Hardware Design for Integrity and Security

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

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.