Made to Order: Verifying Correctness and Security of Hardware through Event Orderings
Monday,
March 4, 2019
11:40 AM
Department of Computer Science, 500 W. 120th St., New York, New York 10027
Room/Area: 451
Room/Area: 451
Computer Science Faculty Recruiting Colloquium - Caroline Trippel
Abstract:
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.
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 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.
Abstract:
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.
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 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.
LOCATION:
← BACK TO EVENTS
- Morningside
- Lecture
- Computer Science
- Alumni
- Faculty
- Family-friendly
- Graduate Students
- Postdocs
- Prospective Students
- Public
- Staff
- Students
- Trainees
Date Navigation Widget
Getting to Columbia
Other Calendars
- Alumni Events
- Barnard College
- Columbia Business School
- Columbia College
- Committee on Global Thought
- Heyman Center
- Jewish Theological Seminary
- Miller Theatre
- School of Engineering & Applied Science
- School of Social Work
- Teachers College
Guests With Disabilities
- Columbia University makes every effort to accommodate individuals with disabilities. Please notify us if you need any assistance by contacting the event’s point person. Alternatively, the Office of Disability Services can be reached at 212.854.2388 and [email protected]. Thank you.