SHF: Small: Exploring Architectural Support for Full-Stack Equational Reasoning in Critical Embedded Systems

SHF：小型：探索关键嵌入式系统中全栈方程推理的架构支持

• 批准号: 1717779
• 负责人: Timothy Sherwood
• 金额: $ 44.99万
• 依托单位: University of California-Santa Barbara
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-07-15 至 2021-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1717779&HistoricalAwards=false
• 关键词: SHF; Small; Exploring; Architectural; Support

In addition to their usual roles in our everyday lives computers also play invisible safety-critical roles. They prevent the brakes in cars from locking up, fly our airplanes through dense air traffic and around large storms, manage our electrical and water systems, and even control the beating of patients' hearts. Unfortunately, it still remains difficult to build computer systems for which one can say anything definitive about reliability of such operation. This project attempts to change the way in which critical computer systems are designed and analyzed. The technologies created will be available and accessible through open repositories, the development of those technologies will provide both undergraduate and graduate students numerous training opportunities, the most exciting ideas will be used in outreach efforts to help reach new generations of engineers, and in the end will help to develop a national community of embedded systems engineers with the skills and tools necessary to implement safe and reliable systems. To achieve this vision of more robust computer controlled systems we need new approaches to creating them that includes both the hardware and the software together. Traditional computer hardware is built for speed and efficiency at all costs, but often we have more than enough speed and efficiency to get a job done. Instead, we need systems that, while remaining quite efficient, also are far easier to understand and reason about. Building on top of powerful theories of computation (such as lambda-calculus) a new computer system, where every action it takes corresponds directly to a tractable set of equations, can be created. Rather than try and solve the resulting equations by hand, this project reconsiders the way computer processors are designed from the ground up so that they work in perfect harmony with state-of-the-art computer-automated theorem provers. To demonstrate that this approach is actually useful on real world problems the investigators are building a completely new computer system around this approach with all of the hardware design, computer languages, and operating system-like software needed.

除了在我们日常生活中扮演的常见角色之外，计算机还扮演着看不见的安全关键角色。 它们可以防止汽车刹车锁死，让我们的飞机穿过密集的空中交通和大风暴，管理我们的电力和供水系统，甚至控制病人的心脏跳动。 不幸的是，构建能够确定其运行可靠性的计算机系统仍然很困难。该项目试图改变关键计算机系统的设计和分析方式。创建的技术将通过开放存储库提供和访问，这些技术的开发将为本科生和研究生提供大量的培训机会，最令人兴奋的想法将用于外展工作，以帮助接触新一代工程师，最终将有助于发展一个全国性的嵌入式系统工程师社区，拥有实施安全可靠系统所需的技能和工具。为了实现更强大的计算机控制系统的愿景，我们需要新的方法来创建它们，包括硬件和软件。 传统的计算机硬件是为了速度和效率而不惜一切代价而构建的，但通常我们有足够的速度和效率来完成工作。 相反，我们需要的系统在保持相当高效的同时，也更容易理解和推理。 建立在强大的计算理论（例如 lambda 演算）之上，可以创建一个新的计算机系统，其中它所采取的每个动作都直接对应于一组易于处理的方程。 该项目不是尝试手动求解所得方程，而是重新考虑计算机处理器的设计方式，以便它们与最先进的计算机自动化定理证明器完美协调工作。 为了证明这种方法实际上对解决现实世界的问题有用，研究人员正在围绕这种方法构建一个全新的计算机系统，其中包含所需的所有硬件设计、计算机语言和类似操作系统的软件。

项目成果

Language Support for Navigating Architecture Design in Closed Form

以封闭形式导航架构设计的语言支持

• DOI: 10.1145/3360047
• 发表时间: 2019-10-25
• 期刊: ACM Journal on Emerging Technologies in Computing Systems (JETC)
• 作者: Weilong Cui;Georgios Tzimpragos;Y. Tao;Joseph McMahan;Deeksha Dangwal;Nestan Tsiskaridze;George Michelogiannakis
• 通讯作者: George Michelogiannakis

Trace Wringing for Program Trace Privacy

程序跟踪隐私的跟踪提取

• DOI: 10.1109/mm.2020.2986113
• 发表时间: 2020-04
• 期刊: IEEE Micro
• 影响因子: 3.6
• 作者: Dangwal, Deeksha;Cui, Weilong;McMahan, Joseph;Sherwood, Tim
• 通讯作者: Sherwood, Tim

Hiding Intermittent Information Leakage with Architectural Support for Blinking

通过闪烁的架构支持隐藏间歇性信息泄漏

• DOI: 10.1109/isca.2018.00059
• 发表时间: 2018-06
• 期刊: Proceedings of the 45th Annual International Symposium on Computer Architecture
• 作者: Althoff, Alric;McMahan, Joseph;Vega, Luis;Davidson, Scott;Sherwood, Timothy;Taylor, Michael;Kastner, Ryan
• 通讯作者: Kastner, Ryan

Bouncer: static program analysis in hardware

Bouncer：硬件中的静态程序分析

• DOI: 10.1145/3307650.3322256
• 发表时间: 2019-06
• 期刊: Proceedings of the 46th International Symposium on Computer Architecture
• 作者: McMahan, Joseph;Christensen, Michael;Dewey, Kyle;Hardekopf, Ben;Sherwood, Timothy
• 通讯作者: Sherwood, Timothy

An Architecture for Analysis

分析架构

• DOI: 10.1109/mm.2018.032271067
• 发表时间: 2018-05
• 期刊: IEEE Micro
• 影响因子: 3.6
• 作者: McMahan, Joseph;Christensen, Michael;Nichols, Lawton;Roesch, Jared;Guo, Sung;Hardekopf, Ben;Sherwood, Timothy
• 通讯作者: Sherwood, Timothy