CAREER: Scalable Assurance via Verifiable Hardware-Software Contracts

职业：通过可验证的硬件软件合同提供可扩展的保证

• 批准号: 2236855
• 负责人: Caroline Trippel
• 金额: $ 57.5万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-02-01 至 2028-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2236855&HistoricalAwards=false
• 关键词: CAREER; Scalable; Assurance; via; Verifiable

Hardware-software (HW-SW) contracts are critical for high-assurance computer systems design and an enabler for software design/analysis tools that find and repair hardware-related bugs in programs. For example, memory consistency models (MCMs) define what values shared memory loads can return in a parallel program. Emerging security contracts define what program data is susceptible to leakage via hardware side-channels. Unfortunately, these contracts and the analyses they support are useless if we cannot guarantee microarchitectural compliance, which is a “grand challenge.” The project's key novelty is a bottom-up approach to the contract verification challenge that synthesizes HW-SW contracts, specifically MCMs and security contracts, from advanced (i.e., industry-scale/complexity) processor implementations. This project's core impacts are as follows. First, a significant fraction of modern design effort is devoted to verification. An automated methodology for synthesizing HW-SW contracts directly from implementations, even with modest designer input, would be a huge step forward. Second, hardware side-channel attacks are arguably the security threat in computer architecture. An approach for precisely computing how a microarchitecture can leak the data it processes through side-channels has direct applications to secure software design and hardware verification today (e.g., verification of Arm’s Data-Independent Timing extensions or Intel’s Operand Independent Timing specification) and HW-SW-security co-design tomorrow.This work will explore three research thrusts to enable synthesizing HW-SW contracts from advanced processor designs. Thrust 1 will investigate what design information is required to support automated contract synthesis procedures and how to acquire it from the target microarchitecture with minimal designer input. Thrust 2 will study how to use the design information acquired in Thrust 1 to develop HW-SW contract synthesis procedures. Thrust 3 will use the contracts produced by Thrust 2 to support hardware verification and program analysis flows rooted in hardware reality. This work's bottom-up approach to verifying contract compliance by synthesizing HW-SW contracts from implementations offers efficiency and scalability advantages over traditional top-down techniques since abstract contracts can be incrementally constructed by evaluating a design’s adherence to simple low-level properties. Moreover, it is robust to HW-SW contracts that emerge post-deployment or evolve over time. HW-SW contracts that are synthesized from implementations enable advances in high-assurance software design and hardware verification. For example, this project will enable the design of software which is provably robust to hardware side-channel leakage as well as comprehensive MCM verification of advanced processor Register Transfer Level (RTL) for the first time. This cross-disciplinary research project cuts across three areas: computer architecture, formal methods, security. The team consists of one PI and a graduate student researcher at Stanford University, who will work with ARM and Intel as partners.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

硬件软件（HW-SW）合同对于高保证计算机系统设计和软件设计/分析工具的推动力至关重要，这些工具可以在程序中查找和修复与硬件相关的错误。例如，内存一致性模型（MCMS）定义哪些值共享内存负载可以在并行程序中返回。新兴的安全合同定义了哪些程序数据容易通过硬件侧通道泄漏。不幸的是，如果我们不能保证微体系依从性，这是“巨大的挑战”，这些合同及其支持的分析将是有用的。该项目的主要新颖性是对合同验证挑战的自下而上的方法，该方法从高级（即行业规模/复杂性）处理器实施中综合了HW-SW合同，特别是MCMS和安全合同。该项目的核心影响如下。首先，现代设计工作的很大一部分用于验证。即使使用适度的设计师输入，也可以直接从实施中综合HW-SW合同的自动化方法是向前迈出的一大步。其次，硬件侧通道攻击可以说是计算机体系结构中的安全威胁。一种精确计算微体系结构如何泄漏通过侧渠道处理的数据的方法直接应用程序，以确保当今的软件设计和硬件验证（例如，验证ARM与数据独立的时间扩展程序或Intel独立的时间和独立的时机规范）以及HW-SW-SW-Security Co-co-designsign。这项工作将探索三项研究作用，以使高级处理器设计的HW-SW合同能够合成。推力1将调查需要哪些设计信息来支持自动合同合成程序以及如何使用最小的设计师输入从目标微体系结构中获取它。推力2将研究如何使用推力1中获得的设计信息来开发HW-SW合同合成程序。推力3将使用推力2产生的合同来支持植根于硬件现实的硬件验证和程序分析流。这项工作的自下而上的方法是通过从实施中综合HW-SW合同来验证合同合规性的方法，这比传统的自上而下技术具有效率和可伸缩性优势，因为可以通过评估设计设计对简单的低级属性的遵守来逐步构建。此外，随着时间的流逝，HW-SW合同出现或进化是强大的。从实现中综合的HW-SW合同可以在高保证软件设计和硬件验证方面的进步。例如，该项目将启用软件的设计，这可能是对硬件侧通道泄漏以及首次对高级处理器寄存器传输级别（RTL）的全面验证的稳健设计。该跨学科研究项目削减了三个领域：计算机架构，正式方法，安全性。该团队由斯坦福大学的一名PI和一名研究生研究员组成，他们将与ARM和Intel合作作为合作伙伴。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的评估评估标准来通过评估来支持的。

项目成果

Serberus: Protecting Cryptographic Code from Spectres at Compile-Time

Serberus：在编译时保护加密代码免受幽灵影响

• 发表时间: 2024
• 期刊: Proceedings of the IEEE Symposium on Security and Privacy
• 作者: Mosier, Nicholas;Nemati, Hamed;Mitchell, John C.;Trippel, Caroline
• 通讯作者: Trippel, Caroline