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

SHF：中：协作研究：使用门级分析构建具有可验证属性的关键系统

• 批准号: 1162177
• 负责人: Ryan Kastner
• 金额: $ 40万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2015-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1162177&HistoricalAwards=false
• 关键词: SHF; Medium; Collaborative; Research; Building

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.

在过去的40年中，计算机性能增加了一倍，但是用于实现这些性能增长的技术使得构建可证明安全，安全或可靠的系统变得越来越困难。这一事实极大地阻碍了我们最安全关键的嵌入式系统的发展，例如医疗，航空，汽车和军事系统中发现的系统。 需要创建这些系统的方式的转换，该系统使用新的硬件设计技术，计算机架构和编程语言来创建具有正式和可证明的安全性属性的类别的硬件/软件系统，这些属性一直可验证到一直到该研究将改变硬件和嵌入式系统设计人员处理可证明属性的问题的方式，使他们能够直接控制和分析系统以最低级别的水平，并在静态地确定其设计是否合规，从而改变了硬件和嵌入式系统设计人员的问题的方式具有给定的政策。 例如，如果必须实时实时系统，则可以通过确保架构设计仔细地通过一组新硬件原始图（旨在利用这些新的原始图片）的软件来仔细管理干扰，从而可以对整个系统进行验证。 ，专门的硬件分析工具和新的设计语言。 为了确保这项技术将影响超出学术界的影响，PIS PIS正在使这些新技术可用，并可以通过易于使用的工具进行访问，并继续在各个级别的研究中包括本科生，以帮助培训能够设计安全至关重要系统的新一代工程师，并将信息保证的概念整合到其广泛的外展活动中。 从长远来看，这项研究将有助于创建嵌入式系统工程师需要评估其系统可信度所需的技能和工具，并且它将减轻我们所有人都为了安全和生计而依靠的关键系统的开发。