Check: Research Tools and Papers

Princeton University

New!

  • January 2022: Daniel Lustig, Caroline Trippel, and Yatin Manerkar have graduated with their PhDs. Some of their subsequent research continues from the Check project at their respective institutions. Please find further updates to such research on their linked webpages.

Overview

From 2013 to the present, our work on specifying, verifying and translating memory consistency models has led to a number of publications, tool releases, and industry adoption.

Perhaps most importantly for a verification project, our verification tools have found numerous major design errors at this point. These include:
  • New speculative execution attack varaints affecting Intel processors (more info).
  • Fundamental deficiencies in the draft specification of a widely-discussed instruction set architecture (more info).
  • An error in the consistency implementation for a widely used simulator (more info).
  • A corner case in a proposed lazy coherence method (more info)(updated spec).
  • Errors in compiler mappings for translating high-level synchronization primitives onto particular instruction sets with weak memory model. And, an error in the formal proof previously thought to ensure the correctness of those mappings (more info).
  • An error in the RTL implementation of memory in an open-source processor. (more info).
Beyond these concrete bug discoveries, our tools have also been used to reproduce other known bugs and deepen understanding of them.

pipecheck



pipecheck

Tool Releases

  • PipeCheck: For verifying that the memory ordering provided by a particular microarchitectural implementation match that of the architectural memory model specification. (github)

  • CCICheck: For verifying coherence and consistency implementations in a unified manner. (github)

  • Web Interface: For building intuition about memory ordering and microarchitectural modeling and verification. (web interface to tool)

  • COATCheck: For verifying memory ordering issues in the face of virtual memory issues (virtual to physical page mappings) and other Hardware-OS Interface issues. (github)

  • ArMOR: For automatically specifying and translating between memory consistency models. (github)

  • TriCheck: Full-Stack MCM verification from high-level languages (e.g. C11) to microarchitectures. (github)

  • RTLCheck: For memory consistency verification of processor RTL against microarchitectural ordering specifications. (github)

  • PipeProof: For memory consistency verification of microarchitectural ordering specifications against ISA-level memory consistency models across all possible programs (an infinite set!). (github)

  • CheckMate: For evaluating hardware susceptibility to classes of security exploits and synthesizing proof-of-concept exploit code when applicable. (github)

  • TransForm: For formally specifying memory transistency models and automatically synthesizing enhanced litmus test suites. (github)

Press

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

Publications

Our work has been supported in part by the National Science Foundation*(under grants CCF-1117147, CCF-1253700, and others). (Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. In addition, we acknowledge past or ongoing support from CFAR, DARPA and others. The provided papers are subject to copyright by ACM, IEEE, or other entities.
  • Naorin Hossain, Caroline Trippel, and Margaret Martonosi. "TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests", the 47th International Symposium on Computer Architecture (ISCA), May-June 2020. *Updated Aug. 1, 2020* (pdf)

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

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Aarti Gupta. "PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications", the 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2018. Nominated for Best Paper. (pdf)

  • Caroline Trippel, Daniel Lustig, and Margaret Martonosi. "CheckMate: Automated Exploit Program Generation for Hardware Security Verification", the 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2018. (pdf)

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

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

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. "RTLCheck: Verifying the Memory Consistency of RTL Designs", the 50th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2017. (pdf)

  • Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee, "Transistency Models: Memory Ordering at the Hardware-OS Interfaces". IEEE Micro, 37 (3) (Top Picks of the 2016 Computer Architecture Conferences), May-June 2017

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

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

  • Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee, "COATCheck: Verifying Memory Ordering at the Hardware-OS Interface", the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2016. (pdf)

  • Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. "CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface", the 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), December 2015. Nominated for Best Paper. (pdf) (slides) (poster)

  • Daniel Lustig, "Specifying, Verifying, and Translating Between Memory Consistency Models", Ph.D. Dissertation, November 2015. Honorable Mention, Bede Liu EE Department Dissertation Award (pdf)

  • Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi, "ArMOR: Defending Against Consistency Model Mismatches in Heterogeneous Architectures", the 42nd International Symposium on Computer Architecture (ISCA), June 2015. (pdf) (extended pdf and gallery) (slides)

  • Daniel Lustig, Michael Pellauer, and Margaret Martonosi, "Verifying Correct Microarchitectural Enforcement of Memory Consistency Models." IEEE Micro, 35 (3) (Top Picks of the 2014 Computer Architecture Conferences), May-June 2015 (pdf)

  • Daniel Lustig, Michael Pellauer, and Margaret Martonosi. PipeCheck: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models. 47th Annual IEEE/ACM International Symposium on Microarchitecture. December, 2014. Nominated for Best Paper Award. (pdf)

People

Tutorial

    We gave a tutorial about our tool suite on the morning of Saturday June 22, 2019 at FCRC in Phoenix. The tutorial webpage contains slides and a virtual machine containing tools and code for the hands-on examples.

https://mrmgroup.cs.princeton.edu/