CheckMate: Automated synthesis of hardware exploits and security litmus tests

Caroline Trippel, Daniel Lustig, Margaret Rose Martonosi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

46 Scopus citations


Recent research has uncovered a broad class of security vulnerabilities in which confidential data is leaked through programmer-observable microarchitectural state. In this paper, we present CheckMate, a rigorous approach and automated tool for determining if a microarchitecture is susceptible to specified classes of security exploits, and for synthesizing proof-of-concept exploit code when it is. Our approach adopts 'microarchitecturally happens-before' (μhb) graphs which prior work designed to capture the subtle orderings and interleavings of hardware execution events when programs run on a microarchitecture. CheckMate extends μhb graphs to facilitate modeling of security exploit scenarios and hardware execution patterns indicative of classes of exploits. Furthermore, it leverages relational model finding techniques to enable automated exploit program synthesis from microarchitecture and exploit pattern specifications. As a case study, we use CheckMate to evaluate the susceptibility of a speculative out-of-order processor to Flush+Reload cache side-channel attacks. The automatically synthesized results are programs representative of Meltdown and Spectre attacks. We then evaluate the same processor on its susceptibility to a different timing side-channel attack: Prime+Probe. Here, CheckMate synthesized new exploits that are similar to Meltdown and Spectre in that they leverage speculative execution, but unique in that they exploit distinct microarchitectural behaviors-speculative cache line invalidations rather than speculative cache pollution-to form a side-channel. Most importantly, our results validate the CheckMate approach to formal hardware security verification and the ability of the CheckMate tool to detect real-world vulnerabilities.

Original languageEnglish (US)
Title of host publicationProceedings - 51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018
PublisherIEEE Computer Society
Number of pages14
ISBN (Electronic)9781538662403
StatePublished - Dec 12 2018
Event51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018 - Fukuoka, Japan
Duration: Oct 20 2018Oct 24 2018

Publication series

NameProceedings of the Annual International Symposium on Microarchitecture, MICRO
ISSN (Print)1072-4451


Other51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture


  • Automated verification
  • Exploit synthesis
  • Hardware security
  • Relational model finding
  • Side-channel attacks


Dive into the research topics of 'CheckMate: Automated synthesis of hardware exploits and security litmus tests'. Together they form a unique fingerprint.

Cite this