I am an Assistant Professor (starting September 2020) in the Computer Science Department at Stanford University. Prior to starting at Stanford, I spent a year as a Research Scientist at Facebook in the FAIR SysML Research 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. 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.
- 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), May-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.
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