Hardware-software (HW-SW) contracts are critical for high-assurance computer systems design and anenabler for software design/analysis tools that find and repair hardware-related bugs in programs. E.g.,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. However, these contracts and the analyses they support are useless if we cannot guarantee microarchitectural compliance, which is a “grand challenge.” Notably, some contracts are still evolving (e.g., security contracts), making hardware compliance a moving target. Even for mature contracts, comprehensively verifying that a complex microarchitecture implements some abstract contract is a time-consuming endeavor involving teams of engineers, which typically requires resorting to incomplete proofs. My talk will give an overview of our recent memory consistency and security verification work, which takes a radically different approach to the challenge above by synthesizing HW-SW contracts from advanced processor implementations.

 Speaker Bio:  

Prof. Caroline Trippel is an assistant professor in the Computer Science and Electrical Engineering Departments at Stanford University. Her research interests are in the area of computer architecture, with a focus on promoting correctness and security as first-order computer systems design metrics. A central theme of her work is leveraging formal methods techniques to design and verify hardware systems. Caroline’s research has been recognized with IEEE Top Picks distinctions, an NSF CAREER Award, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering.