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

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

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.