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）合同对于高保证计算机系统设计至关重要，并且是软件设计/分析工具的推动者，这些工具可以发现和修复程序中与硬件相关的错误。例如，内存一致性模型（MCM）定义了共享内存加载在并行程序中可以返回什么值。新兴的安全合同定义了哪些程序数据容易通过硬件侧通道泄漏。不幸的是，如果我们不能保证微架构的遵从性，这些契约和它们支持的分析就毫无用处，这是一个“巨大的挑战”。该项目的关键新奇是对合同验证挑战的自下而上的方法，该方法综合了HW-SW合同，特别是MCM和安全合同，从高级（即，工业规模/复杂度）处理器实现。该项目的核心影响如下。首先，现代设计工作的很大一部分用于验证。一种直接从实现中合成HW-SW合同的自动化方法，即使有适度的设计师输入，也将是一个巨大的进步。其次，硬件侧信道攻击可以说是计算机体系结构中的安全威胁。一种用于精确计算微体系结构如何通过侧信道泄漏其处理的数据的方法直接应用于当今的安全软件设计和硬件验证（例如，Arm的Data-Independent Timing extensions或Intel的Operand Independent Timing specification的验证）和HW-SW-security co-design。这项工作将探索三个研究方向，以实现从高级处理器设计中合成HW-SW合同。重点1将研究需要什么设计信息来支持自动化合同合成过程，以及如何以最少的设计人员输入从目标微体系结构中获取这些信息。推力2将研究如何使用推力1中获得的设计信息来开发硬件-软件合同综合程序。Thrust 3将使用Thrust 2生成的合同来支持硬件验证和基于硬件现实的程序分析流程。这项工作的自下而上的方法来验证合同的合规性，综合硬件软件合同的实现提供了效率和可扩展性的优势，传统的自上而下的技术，因为抽象的合同可以逐步构建通过评估设计的坚持简单的低级别的属性。此外，它对部署后出现或随着时间的推移而演变的HW-SW合同具有鲁棒性。从实施中合成的HW-SW合同可以促进高保证软件设计和硬件验证。例如，该项目将使软件的设计，这是证明强大的硬件侧通道泄漏，以及全面的MCM验证先进的处理器寄存器传输级（RTL）的第一次。这个跨学科的研究项目跨越三个领域：计算机体系结构，形式化方法，安全性。该团队由斯坦福大学的一名PI和一名研究生研究员组成，他们将与ARM和英特尔合作。该奖项反映了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