Research
I am an Assistant Professor in the Computer Science and Electrical Engineering Departments at Stanford University, where I lead the High Assurance Computer Architectures Lab. 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.
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 NSF CAREER Award (2023), 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
- EuroSys '24"Model Selection for Latency-Critical Inference Serving". Daniel Mendoza, Francisco Romero, and Caroline Trippel. In Proceedings of the 15th European COnference on Computer Systems (EuroSys), April 2024.
- S&P '24"Serberus: Protecting Cryptographic Code from Spectres at Compile Time". Nicholas Mosier, Hamed Nemati, John C. Mitchell, and Caroline Trippel. In Proceedings of the 45th IEEE Symposium on Security and Privacy, May 2024.
- CAV '23"nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models". Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. In Proceedings of the 34th International Conference on Computer Aided Verification, July 2023.
- DAC '23"G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators". Saranyu Chattopadhyay, Keerthikumara Devarajegowda, Bihan Zhao, Florian Lonsing, Brandon A. D'Agostino, Ioanna Vavelidou, Vijay D. Bhatt, Sebastian Prebeck, Wolfgang Ecker, Caroline Trippel, Clark Barrett, Subhasish Mitra. In Proceedings of the 60th Design Automation Conference, July 2023.
- 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 A-QED 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 '21Jose 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 NSF CAREER Award (2023)
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:
- TechSpot: "Researchers discover two new Spectre and Meltdown variants."
- Digital Trends: "New ‘Prime’ Meltdown, Spectre exploits outlined by Nvidia, Princeton University"
- Gizmodo: "Researchers Find New Ways to Exploit Meltdown and Spectre Vulnerabilities in Modern CPUs"
- Hacker News: "MeltdownPrime, SpectrePrime: Exploiting Invalidation-Based Coherence Protocol"
- Tech Xplore: "MeltdownPrime and SpectrePrime: Researchers nail exploits"
- Engadget: "Researchers discover new ways to abuse Meltdown and Spectre flaws"
April, 2017. TriCheck and deficiences in the RISC-V ISA MCM Specification:
- Princeton Press Release
- RISC-V Response
- Phys.org: "Tool checks computer architectures, reveals flaws in emerging design"
- System Bits: "April 18 – RISC-V errors; spin-wave logic gates; deep learning is old"
- Electronics Weekly: "RISC-V bugs found by Princeton"
- Electronic Design "Memory Ordering Flaw Found in Rare Version of RISC-V Hardware"
- Design and Reuse. "RISC-V: When a bug really is a feature"
March, 2016. STARNet Center for Future Architectures Research (CFAR):
- March, 2016: STARNet Center for Future Architectures Research (CFAR) coverage of our work