05-29

Specification and Formal Verification of Hardware-Software Contracts for High-Assurance Computer Architectures

The complexity of modern computer systems gives rise to two critical computer architecture challenges: traditional instruction set architectures lack the detail needed to capture how hardware may undermine software assurance—correctness, security, reliability; and verification is a major and growing hardware design bottleneck, with critical bugs escaping to silicon in >85% of hardware projects despite verification consuming >50% of design effort, per a 2024 Siemens EDA study. To address these challenges, our work develops hardware-software (HW-SW) contracts to support software assurance and automated approaches and tools to rigorously verify hardware implementations against them.

This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs. I will present three different tools built on this unified approach for side-channel security, memory consistency, and cache coherence verification of processor implementations. I will also briefly highlight our contracts work, which prompted Intel to update their Software Security Guidance and is informing industrial discussions on retrofitting the Arm ISA to better support performant constant-time code in the Spectre era of microarchitectural side-channel attacks.

Bio: Caroline Trippel is an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University, where she leads the High Assurance Computer Architectures Lab. A central theme of her work is leveraging formal methods, especially automated reasoning, techniques to design and verify hardware systems. Trippel's research has been recognized with IEEE Top Picks and Best Paper Award distinctions, a Sloan Research Fellowship, an NSF CAREER Award, the inaugural Google ML and Systems Junior Faculty Award, the Intel Rising Star Faculty Award, an Intel Outstanding Researcher Award, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering.