CAREER: Scalable Assurance via Verifiable Hardware-Software Contracts

硬件-软件(HW-SW)合同对于高保证的计算机系统设计至关重要，也是软件设计/分析工具的推动者，软件设计/分析工具可以发现和修复程序中与硬件相关的错误。例如，内存一致性模型(MCM)定义了共享内存加载可以在并行程序中返回什么值。新兴的安全合同定义了哪些程序数据容易通过硬件旁路泄露。不幸的是，如果我们不能保证微体系结构遵从性，那么这些合同和它们所支持的分析就毫无用处了，这是一个“巨大的挑战”。该项目的主要创新是采用自下而上的方法来应对合同验证挑战，该方法从高级(即行业规模/复杂性)处理器实现中综合了硬件-软件合同，特别是MCM和安全合同。该项目的核心影响如下。首先，现代设计的很大一部分工作都致力于验证。一种直接从实现中合成硬件-软件合同的自动化方法，即使只需少量的设计师输入，也将是向前迈出的一大步。其次，硬件侧通道攻击可以说是计算机体系结构中的安全威胁。一种精确计算微体系结构如何通过旁路泄漏其处理的数据的方法将直接应用于今天的软件设计和硬件验证(例如，验证ARM的与数据无关的时序扩展或英特尔的与操作数无关的时序规范)和明天的硬件-软件-安全联合设计。这项工作将探索三个研究推动力，以使能够从高级处理器设计合成硬件-软件合同。推力1将调查支持自动合同合成程序所需的设计信息，以及如何以最少的设计者投入从目标微体系结构中获取这些信息。推力2将研究如何利用在推力1中获得的设计信息来制定硬件-软件合同综合程序。推力3将使用推力2产生的合同来支持硬件验证和植根于硬件现实的程序分析流程。这项工作的自底向上方法通过从实现中合成硬件-软件合同来验证合同遵从性，与传统的自上而下技术相比，提供了效率和可伸缩性优势，因为抽象合同可以通过评估设计对简单低级属性的遵守来增量地构建。此外，它对部署后出现或随时间发展的硬件-软件合同具有很强的适应性。从实施中合成的硬件-软件合同可在高保证的软件设计和硬件验证方面取得进展。例如，该项目将使软件的设计能够证明对硬件侧通道泄漏具有健壮性，以及首次对高级处理器寄存器传输级别(RTL)进行全面的MCM验证。这个跨学科的研究项目横跨三个领域：计算机体系结构、形式化方法、安全。该团队由一名PI和一名斯坦福大学的研究生研究员组成，他们将作为合作伙伴与ARM和英特尔合作。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.