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

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

• 批准号: 1162187
• 负责人: Timothy Sherwood
• 金额: $ 79.99万
• 依托单位: University of California-Santa Barbara
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1162187&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 年里，计算机性能翻了很多倍，但用于实现这些性能提升的技术却使得构建可证明安全、可靠的系统变得越来越困难。这一事实极大地阻碍了我们最安全关键的嵌入式系统（例如医疗、航空电子、汽车和军事系统中的嵌入式系统）的开发进展。 需要对这些系统的创建方式进行转变，即使用新的硬件设计技术、计算机架构和编程语言来创建具有正式且可证明的安全属性的硬件/软件系统类别，这些属性可以一直被验证到位和逻辑门的实现级别。这项研究将改变硬件和嵌入式系统设计人员处理可证明属性问题的方式，使他们能够在最低级别直接控制和分析系统，并静态确定他们的设计是否符合要求与给定的政策。 例如，如果一个系统必须是实时的，那么通过确保架构设计通过一组新的硬件原语和设计用于利用这些新原语的软件来仔细管理干扰，这个属性对于整个系统（从门到软件）都是可验证的、专门的硬件分析工具和新的设计语言。 为了确保这项技术能够对学术界以外的领域产生影响，PI 正在通过易于使用的工具提供和访问这些新技术，并继续让各级研究的本科生参与其中，以帮助培训能够设计安全关键系统的新一代工程师，并将信息保障的概念融入其广泛的外展活动中。 从长远来看，这项研究将有助于创建嵌入式系统工程师评估其系统可信度所需的技能和工具，并将简化我们所有人的安全和生计所依赖的关键系统的开发。