CAREER: Scalable Assurance via Verifiable Hardware-Software Contracts

点击翻译按钮获取中文摘要

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.