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.