Skip to main content

CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests

Author(s): Trippel, Caroline; Lustig, Daniel; Martonosi, Margaret

To refer to this page use:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorTrippel, Caroline-
dc.contributor.authorLustig, Daniel-
dc.contributor.authorMartonosi, Margaret-
dc.identifier.citationTrippel, Caroline, Daniel Lustig, and Margaret Martonosi. "CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests." 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO) (2018): pp. 947-960. doi:10.1109/MICRO.2018.00081en_US
dc.description.abstractRecent 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.en_US
dc.format.extent947 - 960en_US
dc.relation.ispartof51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO)en_US
dc.rightsAuthor's manuscripten_US
dc.titleCheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Testsen_US
dc.typeConference Articleen_US

Files in This Item:
File Description SizeFormat 
CheckMateHardwareExploitsSecurity.pdf667.88 kBAdobe PDFView/Download

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.