Correctness and security problems in modern computer systems can result from problematic hardware event orderings and interleavings during an application’s execution. Since hardware designs are complex and since a single user-facing instruction can exhibit a variety of different hardware execution sequences, analyzing and verifying systems for correct event orderings is challenging. My work addresses these challenges by combining hardware architecture and systems approaches with formal methods to support the specification, analysis, and verification of implementation-aware event ordering scenarios, with the specific goal of automatically synthesizing implementation-aware programs capable of violating correctness or security guarantees. In this talk, I will present two formal, early-stage verification tools and techniques rooted in this approach. TriCheck conducts axiomatic full-stack memory consistency model (MCM) verification (from high-level programming languages down through hardware implementations). Using rigorous and efficient formal approaches, TriCheck identified flaws in RISC-V’s draft MCM specification and two counterexamples to a previously proven-correct compiler mapping scheme from C11 to IBM Power and ARMv7. Noting that MCM and security analysis are amenable to similar approaches, CheckMate uses related axiomatic techniques to evaluate susceptibility of a hardware design and its related system support to formally-specified classes of security exploits; in response, it synthesizes proof-of-concept exploit code when a design is susceptible. CheckMate automatically synthesized programs representative of Meltdown and Spectre attacks as well as new exploits, MeltdownPrime and SpectrePrime, that I have demonstrated on Intel hardware.
Caroline Trippel is a Ph.D. candidate in the Computer Science Department at Princeton University. She is advised by Professor Margaret Martonosi on her computer architecture dissertation research, specifically on the topic of concurrency and security verification in heterogeneous parallel systems. Her work bridges computer architecture and formal methods and demonstrates the importance of that bridge in specifying and verifying the correct and secure execution of software running on such systems. Trippel has influenced the design of the RISC-V ISA memory consistency model (MCM) both via full-stack MCM analysis of its draft specification and her subsequent participation in the RISC-V Memory Model Task Group; she received recognition for this work via the 2017-2018 NVIDIA Graduate Research Fellowship. Additionally, Trippel has developed a novel methodology and tool that synthesized two new variants of the recently publicized Meltdown and Spectre attacks; this work lead to a funded collaboration with Intel on side-channel attack research. She received her B.S. in Computer Engineering from Purdue University in 2013 and her M.A. in Computer Science from Princeton University in 2015. She will receive her Ph.D. in Computer Science from Princeton University in Spring 2019.