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