Caroline June Trippel

Princeton Computer Science Ph.D. Candidate

About

CV

I am a Ph.D. candidate in the Computer Science Department at Princeton University. I am advised by Professor Margaret Martonosi on my computer architecture dissertation research, specifically on the topic of concurrency and security verification in heterogeneous parallel systems. My 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. My work has influenced the design of the RISC-V ISA memory consistency model (MCM) both via my full-stack MCM analysis of its draft specification and my subsequent participation in the RISC-V Memory Model Task Group; I received recognition for this work via the 2017-2018 NVIDIA Graduate Research Fellowship. Additionally, my work has produced 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. I received my B.S. in Computer Engineering from Purdue University in 2013 and my M.A. in Computer Science from Princeton University in 2015. I will receive my Ph.D. in Computer Science from Princeton University in Spring 2019.







ctrippel_img
uhb_img

Research

Computer Architecture, Parallelism, Heterogeneity, Formal Verification, Memory Consistency Models, Hardware Security
  • Computer architecture
  • Heterogeneous parallel systems interface specification and verification
  • Memory consistency model specification and verification
  • Hardware security verification
  • Heterogeneous memory consistency model design and specification
  • Security interface design and specification
    Published website comprising our verification work
  • Publications

    Refereed

    "Security Verification through Automatic Hardware-Aware Exploit Synthesis: The CheckMate Approach"
    Caroline Trippel, Daniel Lustig, and Margaret Martonosi
    IEEE Micro, 39 (3), May-June 2019.
    Issue: Top Picks from the Computer Architecture Conferences of 2018

    "ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification"
    Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Maronosi, Sharad Malik
    In Proceedings of the 2018 Conference on Formal Methods in Computer Aided Design (FMCAD), October-November 2018.

    "CheckMate: Automated Exploit Program Generation for Hardware Security Verification"
    Caroline Trippel, Daniel Lustig, and Margaret Martonosi
    In Proceedings of the 51st International Symposium on Microarchitecture (MICRO), October 2018

    "Full-Stack Memory Model Verification with TriCheck"
    Caroline Trippel, Yatin Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi
    IEEE Micro, 38 (3), May-June 2018.
    Issue: Top Picks from the Computer Architecture Conferences of 2017

    "TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA"
    Caroline Trippel, Yatin Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi
    In Proceedings of the 22nd International Conference on Architectural Support for
    Programming Languages and Operating Systems (ASPLOS), April 2017

    "ArMOR: Defending Against Consistency Model Mismatches in Heterogeneous Architectures"
    Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi
    In Proceedings of the 42nd International Symposium on Computer Architecture (ISCA), June 2015

    Non-Refereed

    "MeltdownPrime and SpectrePrime: Automatically-Synthesized Attacks Exploiting Invalidation-Based Coherence Protocols"
    Caroline Trippel, Daniel Lustig, and Margaret Martonosi
    CoRR, abs/1802.03802, 2018.

    "Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings"
    Yatin Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi
    CoRR, abs/1611.01507, 2016.

    Selected Presentations

    "CheckMate: Automated Exploit Program Generation for Hardware Security Verification"
    Caroline Trippel, Daniel Lustig, Margaret Martonosi
    51st International Symposium on Microarchitecture (MICRO), October 2018.
    (Lightning Talk)

    "TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA"
    Caroline Trippel, Yatin Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi
    22nd International Conference on Architectural Support for Programming languages and Operating Systems (ASPLOS), April, 2016.

    "A Memory Consistency Model for RISC-V"
    Caroline Trippel
    5th RISC-V Workshop, November 2016.

    Selected Awards and Honors

    Selected for 2018 MIT Rising Stars in EECS Workshop
    Selected for 2018 ACM Heidelberg Laureate Forum
    TriCheck chosen as an IEEE MICRO Top Pick of 2017 (top 12 Computer Architecture papers of 2017)
    NVIDIA Graduate Fellowship Recipient: 2017-2018

    Academic



    princeton_logo


    purdue_logo

    Degrees

    Ph.D. Department of Computer Science, Princeton University, 2013 - 2019

    M.A. Department of Computer Science, Princeton University, 2013 - 2015
    B.S. School of Electrical and Computer Engineering, Purdue University, 2009 - 2013

    Teaching

    Computer Architecture and Organization (COS 375): Fall 2016, instructor Margaret Martonosi Computer Architecture and Organization (COS 375): Fall 2014, instructor Margaret Martonosi

    Graduate Coursework

    Great Moments in Computing (COS 583): Fall 2014, instructor Margaret Martonosi
    Advanced Networks (COS 561): Fall 2014, instructor Jennifer Rexford
    Computer Architecture (ELE 475): Spring 2014, instructor David Wentzlaff
    Programming Languages (COS 510): Spring 2014, instructor David Walker
    Artificial Intelligence (COS 402): Fall 2013, instructor Alexandru Niculescu-Mizil
    Parallel Computation (ELE 575): Fall 2013, instructor David Wentzlaff

    Tutorials

    "Why Memory Consistency Models Matter… And tools for analyzing and verifying them."
    Caroline Trippel and Yatin A. Manerkar
    Uppsala Programming for Multicore Architectures Research Center (UPMARC) Multicore Computing Summer School, June 2018

    "Why Memory Consistency Models Matter… And tools for analyzing and verifying them."
    Yatin A. Manerkar, Caroline Trippel, and Margaret Martonosi
    44th International Symposium on Computer Architecture (ISCA), June, 2017

    Press

    February, 2018: Press regarding CheckMate's synthesis of new variants of Meltdown and Spectre:
    April, 2017: Press regarding TriCheck and deficiences in the RISC-V ISA MCM Specification:
    March, 2016: STARNet Center for Future Architectures Research (CFAR) Coverage of our work

    Contact Information


    213 Computer Science Building
    Department of Computer Science
    Princeton University

    ctrippel (at) cs.princeton.edu