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
Add to Calendar

Link added to clipboard:

https://events.columbia.edu/cal/event/eventView.do?b=de&calPath=%2Fpublic%2Fcals%2FMainCal&guid=CAL-00bb9e28-690a2fb7-0169-0cf25800-00002618events@columbia.edu&recurrenceId=
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.
Event Contact Information:
Luca Carloni
[email protected]
LOCATION:
  • Morningside
TYPE:
  • Lecture
CATEGORY:
  • Computer Science
EVENTS OPEN TO:
  • Alumni
  • Faculty
  • Family-friendly
  • Graduate Students
  • Postdocs
  • Prospective Students
  • Public
  • Staff
  • Students
  • Trainees
BACK TO EVENTS

Date Navigation Widget

Filter By

Subscribe Export Options

Getting to Columbia

Other Calendars

Guests With Disabilities