Research

I am an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University. Prior to starting at Stanford, I spent nine months as a Research Scientist at Facebook in the FAIR SysML group. My research interests are in the area of computer architecture, with a focus on promoting correctness and security as first-order computer systems design metrics (akin to performance and power). A central theme of my work is leveraging formal methods techniques to design and verify hardware systems in order to ensure that they can provide correctness and security guarantees for the applications they intend to support. I have been recently exploring the role of architecture in enabling privacy-preserving machine learning, the role of machine learning in hardware systems optimizations, particularly in the context of neural recommendation, and opportunities for improving datacenter and at-scale machine learning reliability.

My research has influenced the design of the RISC-V ISA memory consistency model both via my formal analysis of its draft specification and my subsequent participation in the RISC-V Memory Model Task Group. Additionally, my work produced a novel methodology and tool that synthesized two new variants of the now-famous Meltdown and Spectre attacks.

My research has been recognized with IEEE Top Picks distinctions, the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award, and the 2020 CGS/ProQuest® Distinguished Dissertation Award in Mathematics, Physical Sciences, & Engineering. I was also awarded an NVIDIA Graduate Fellowship (2017-2018) and selected to attend the 2018 MIT Rising Stars in EECS Workshop. I completed my PhD in Computer Science at Princeton University and my BS in Computer Engineering at Purdue University.

Prospective students: I am currently looking for motivated graduate students, postdoctoral scholars, and undergraduate researchers. Once admitted to Stanford, if you are interested in working with me, please send me an email with your CV to start a conversation.

Publications

  • ISCA '22
    "Axiomatic Hardware-Software Contracts for Security". Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. In Proceedings of the 49th International Symposium on Computer Architecture (ISCA), June 2022.
  • ASPLOS '22
    "RecShard: Statistical Feature-Based Memory Optimization for Industry-Scale Neural Recommendation". Geet Sethi, Bilge Acun, Niket Agarwal, Christos Kozyrakis, Caroline Trippel, and Carole-Jean Wu. In Proceedings of the 27th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), February-March 2022.
  • MICRO '21
    "Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations". Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, and Caroline Trippel. In Proceedings of the 54th International Symposium on Microarchitecture (MICRO), October 2021.
  • FMCAD '21
    "Scaling Up Hardware Accelerator Verification using \aqed with Functional Decomposition". Saranyu Chattopadhyayi, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett, and Subhasish Mitra. In Proceedings of the 2021 Conference on Formal Methods in Computer Aided Design (FMCAD), October 2021.
  • PLDI '21
    "Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption". Meghan Cowan, Deeksha Dangwal, Armin Alaghi, Caroline Trippel, Vincent T. Lee, and Brandon Reagen. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), June 2021.
  • ISCA '21
    Jose Rodrigo Sanchez Vicarte, Pradyumna Shome, Nandeeka Nayak, Caroline Trippel, Adam Morrison, David Kohlbrenner, Christopher W. Fletcher. “Opening Pandora’s Box: A Systematic Study of New Ways Microarchitecture Can Leak Private Data”. In Proceedings of the 48th ACM/IEEE International Symposium on Computer Architecture (ISCA), June 2021.
  • ASPLOS '21
    "RecSSD: Near Data Processing for Solid State Drive Based Recommendation Inference Extended Abstract". Mark Wilkening, Udit Gupta, Samuel Hsia, Caroline Trippel, Carole-Jean Wu, David Brooks, and Gu-Yeon Wei. In Proceedings of the 26th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2021.
  • MLSys '21
    "Understanding and Improving Failure Tolerant Training for Deep Learning Recommendation with Partial Recovery". Kiwan Maeng, Shivam Bharuka, Isabel Gao, Mark Jeffrey, Vikram Saraph, Bor-Yiing Su, Caroline Trippel, Jiyan Yang, Mike Rabbat, Brandon Lucia, and Carole-Jean Wu. In Proceedings of the 3rd Conference on Machine Learning and Systems (MLSys), April 2021.
  • ISCA '20
    "TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests". Naorin Hossain, Caroline Trippel, and Margaret Martonosi. In Proceedings of the 47th International Symposium on Computer Architecture (ISCA), June 2020.
  • Princeton University '19
    "Concurrency and Security Verification in Heterogeneous Parallel Systems". Caroline Trippel. PhD Dissertation. Princeton University. November 2019.
  • TOP PICKS '19
    "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.
  • FMCAD '18
    "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.
  • MICRO '18
    "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.
  • ARXIV '18
    "MeltdownPrime and SpectrePrime: Automatically-Synthesized Attacks Exploiting Invalidation-Based Coherence Protocols". Caroline Trippel, Daniel Lustig, and Margaret Martonosi. CoRR, abs/1802.03802, 2018.
  • TOP PICKS '18
    "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.
  • ASPLOS '17
    "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.
  • ARXIV '16
    "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.
  • ISCA '15
    "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.

Awards & Honors

Recipient of the 2020 CGS/ProQuest® Distinguished Dissertation Award
Recipient of the 2020 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award
CheckMate chosen as an IEEE MICRO Top Pick of 2018 (top 12 computer architecture papers of 2018)
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

Press

February, 2018. CheckMate's synthesis of new variants of Meltdown and Spectre:

April, 2017. TriCheck and deficiences in the RISC-V ISA MCM Specification:

March, 2016. STARNet Center for Future Architectures Research (CFAR):