Caroline Trippel will present her Pre FPO "Concurrency and Security Verification in Heterogeneous Parallel Systems" on Monday, September 10, 2018 at 2pm in CS 402. The members of her committee are as follows: Margaret Martonosi (advisor); Readers: Daniel Lustig (NVIDIA ) and Aarti Gupta; Examiners: Andrew Appel and David Wentzlaff (non-reader). All are welcome to attend. Concurrency and Security Verification in Heterogeneous Parallel Systems Abstract Modern computer systems achieve high performance scaling at manageable power and thermal levels by employing parallelism along with high degrees of specialization and heterogeneity. Parallelism and heterogeneity have been employed for years, but today the increasing degree to which they are used poses grand challenge verification problems regarding the “accuracy” of event orderings in system-wide executions. Memory consistency models (MCMs) are one notable design specification that articulate the event orderings needed to guarantee correctness for concurrent programs. As it turns out, accuracy of event orderings forms the cornerstone of security, as well as concurrency in modern processors. Namely, a significant portion of hardware security vulnerabilities that lead to violations of confidentiality and integrity are similarly related to event orderings. My dissertation creates formal, automated tools and techniques for interactive, early-stage specification and verification of the correctness and security of software executing on heterogeneous parallel systems. To address correctness, 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 align on MCM requirements. In TriCheck’s evaluation of the RISC-V ISA’s support for C11 programs, TriCheck identified fundamental flaws in RISC-V’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 work makes the important and non-obvious observation that the event ordering issues present in hardware MCM analysis are similar to those relevant for hardware security analysis. By re-purposing and augmenting the graph-based MCM analysis techniques above, my work has produced a methodology and tool, CheckMate, for evaluating a microarchitecture’s susceptibility to formally-specified classes of security exploits and for synthesizing proof-of-concept exploit code when it is. Using this tool to evaluate the susceptibility of a speculative out-of-order processor 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 its susceptibility to Prime+Probe attacks generated two new exploits, highlighting the importance of automated verification techniques for identifying hardware security vulnerabilities. Overall, these techniques offer advances that allow architects and system designers to play an important early-stage role in system verification for correctness and security, by offering efficient and high-coverage formal methods on which to explore system designs and their vulnerabilities. Bio 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 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 B.S. in Computer Engineering from Purdue University in 2013, her M.A. in Computer Science from Princeton University in 2015, and was a 2017-2018 NVIDIA Graduate Fellow.