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

14 Scopus citations

Abstract

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
Pages947-960
Number of pages14
ISBN (Electronic)9781538662403
DOIs
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
Volume2018-October
ISSN (Print)1072-4451

Other

Other51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018
CountryJapan
CityFukuoka
Period10/20/1810/24/18

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Keywords

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

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

Cite this