<html><body><div id="zimbraEditorContainer" style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000" class="11"><div class="">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.<br></div><div class=""><br data-mce-bogus="1"></div><div class="">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).</div><div class=""><br data-mce-bogus="1"></div><div class="">All are welcome to attend.</div><div class=""><div><blockquote class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="" data-mce-style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><p class="MsoNormal"><b class=""><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">Concurrency and Security Verification in Heterogeneous
Parallel Systems</span></b></p><p class="MsoNormal"><b class=""><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">Abstract</span></b></p><p class="MsoNormal"><span style="font-size: 10pt;" class="" data-mce-style="font-size: 10pt;">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 </span><span style="font-size: 10pt;" class="" data-mce-style="font-size: 10pt;"> </span><span style="font-size: 10pt;" class="" data-mce-style="font-size: 10pt;">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.</span></p><p class="MsoNormal"><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">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.</span></p><p class="MsoNormal"><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">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.</span></p><p class="MsoNormal"><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">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.</span></p><p class="MsoNormal"><b class=""><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">Bio</span></b></p><p class="MsoNormal"><span style="font-size: 10.0pt;" class="" data-mce-style="font-size: 10.0pt;">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.</span></p><p class="MsoNormal"> </p></div></div></blockquote></div></div><br></div></body></html>