SHF: Medium: Collaborative Research: Building Critical Systems with Verifiable Properties Using Gate Level Analysis

在过去的40年里，计算机性能翻了许多倍，但用来实现这些性能提高的技术本身，使得构建被证明是安全、可靠的系统变得越来越困难。这一事实严重阻碍了我们最关键的安全嵌入式系统的开发，例如医疗、航空电子、汽车和军事系统中的嵌入式系统。需要改变这些系统的创建方式，使用新的硬件设计技术、计算机体系结构和编程语言来创建具有形式化和可证明的安全属性的硬件/软件系统类别，这些属性可以一直验证到位和逻辑门的实现级别。这项研究将改变硬件和嵌入式系统设计人员处理可证明属性问题的方式，使他们能够在最低级别直接控制和分析系统，并静态地确定他们的设计是否符合给定的策略。例如，如果系统必须是实时的，则通过确保体系结构设计通过一组新的硬件原语、设计用于利用这些新原语的软件、专门的硬件分析工具和新的设计语言来小心地管理干扰，可以对整个系统(从门到软件)验证该属性。为了确保这项技术将产生超越学术界的影响，私人投资机构正在通过易于使用的工具使这些新技术可用和可用，继续吸收各级研究的本科生帮助培训能够设计关键安全系统的新一代工程师，并将信息保障的概念纳入其广泛的外联活动中。从长远来看，这项研究将有助于创造嵌入式系统工程师评估其系统可信度所需的技能和工具，并将简化那些我们所有人都依赖于安全和生计的关键系统的开发。

Computer performance has doubled many times over during the past 40 years, but the very techniques used to achieve these performance gains have made it increasingly difficult to build systems that are provably safe, secure, or reliable. This fact significantly impedes progress in the development of our most safety-critical embedded systems such as those found in medical, avionic, automotive, and military systems. A transformation in the way that these systems are created is needed, one that uses new hardware design techniques, computer architectures, and programming languages to create classes of hardware/software systems with formal and provable safety properties that are verifiable all the way down to the implementation level of bits and logic gates.This research will change the way that hardware and embedded systems designers approach the problem of provable properties, enabling them to directly control and analyze the system at the lowest level and to statically determine if their designs are in compliance with a given policy. For example, if a system must be real-time this property can be verifiable for a full system, from gates to software, by ensuring that the architecture design carefully manages interference through a set of new hardware primitives, software designed to exploit these new primitives, specialized hardware analysis tools, and new design languages. To ensure this technology will have impact beyond academia the PIs are making these new technologies available and accessible through easy to use tools, continuing to include undergraduates at all levels of research to help train a new generation of engineers capable of designing safety-critical systems, and integrating concepts from information assurance into their extensive outreach activities. Over the long term this research will help create the skills and tools that embedded system engineers need to evaluate the trustworthiness of their systems, and it will ease the development of those critical systems on which we all depend on for our safety and livelihood.