Position: PhD Candidate
Current Institution: Princeton University
Abstract: Concurrency and Security Verification in Heterogeneous, Parallel Systems
Modern computer systems achieve high performance by employing parallelism and high degrees of specialization and heterogeneity. This scenario presents challenges to reliable and secure systems design. For example, the heterogeneous compute elements make a variety of assumptions about the ordering of synchronization and memory accesses—i.e., they have different memory consistency models (MCMs). Additionally, with more and more functionality being put into hardware, security exploits increasingly attack the implementations on which seemingly secure algorithms are run. My dissertation creates formal automated tools and techniques for specifying and verifying the correct execution of software on heterogeneous parallel systems to improve reliability and security. To address reliability, my work has produced techniques and a novel tool-flow TriCheck for full-stack MCM verification. TriCheck leverages SMT-based analysis of hardware-aware program execution graphs to determine if a specific combination of high-level language compiler ISA and microarchitecture could ever produce an illegal program outcome. In TriCheck’s, evaluation of the RISC-V ISA’s support for C11 programs TriCheck identified fundamental flaws in the RISC-V ISA’s draft MCM specification. This work also identified bugs in two previously “proven-correct” compiler mappings from C11 to IBM Power and ARMv7 leading to the discovery of flaws in C11’s MCM itself. To tackle security, my research adapts and extends the graph-based MCM analysis techniques above. Specifically, my work has produced a methodology and tool for evaluating a microarchitecture’s susceptibility to formally-specified classes of security exploits and automatically synthesizing proof-of-concept exploit code when applicable. Using this tool to evaluate a standard out-of-order processor on its susceptibility to Flush+Reload cache side-channel attacks resulted in automatically synthesized programs representative of those that were publicly disclosed for conducting Meltdown and Spectre attacks. Evaluating the same processor on susceptibility to Prime+Probe attacks generated two new exploits highlighting the importance of automated verification techniques for identifying hardware security vulnerabilities.
Caroline Trippel is a PhD candidate in the Computer Science Department at Princeton, advised by Professor Margaret Martonosi. Her work has resulted in formal, automated tools and techniques for specifying and verifying the correct and secure execution of software running on such systems. She 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. Additionally, she has developed a novel methodology and tool that synthesized two new variants of the recently publicized Meltdown and Spectre attacks. Caroline received her bachelor’s degree in Computer Engineering from Purdue University in 2013, a master’s in computer science from Princeton University in 2015, and was a 2017-2018 NVIDIA Graduate Fellow.