Abstract: The security of modern software ultimately depends on the hardware on which it is run. Thus, it is essential that hardware designers (1) expose security-relevant implementation details to application developers via hardware-software contracts, and (2) ensure (ideally through formal approaches) that said contracts are indeed upheld by fabricated microarchitectures. Unfortunately, microarchitectural attacks—side-channel attacks which leak data processed by programs as a direct result of hardware optimizations—demonstrate a notable deficiency in how existing hardware-software contracts define software visible state. My talk will cover our solution to this shortcoming—axiomatic hardware-software contracts for security (i.e., security contracts), called leakage containment models (LCMs), which support formally reasoning about the security guarantees of programs when they run on particular microarchitectures. Using LCMs, we formally define microarchitectural leakage, so that it can be automatically detected in programs. As a proof of concept, we use LCMs to design a static analysis tool which has automatically identified novel microarchitecture vulnerabilities real-world crypto-libraries—OpenSSL and Libsodium. To conclude my talk, I will give insight into our latest work on synthesizing security contracts, such as LCMs, from processor RTL directly as a way to ensure hardware-contract compliance.

Bio: Caroline Trippel is an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University working in the area of computer architecture. A central theme of her work is leveraging formal methods techniques to design and verify hardware systems in order to ensure that they can provide correctness and security guarantees for the applications they intend to support. Trippel’s research has influenced the design of the RISC-V ISA memory consistency model both via her formal analysis of its draft specification and her subsequent participation in the RISC-V Memory Model Task Group. Additionally, her work produced a novel methodology and tool that synthesized two new variants of the now-famous Meltdown and Spectre attacks. Trippel’s research has been recognized with IEEE Top Picks distinctions, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering. She was also awarded an NVIDIA Graduate Fellowship (2017-2018) and selected to attend the 2018 MIT Rising Stars in EECS Workshop.