Speccheck: A Tool for Systematic Identification of Vulnerable Transient Execution in gem5

Graduate Thesis Or Dissertation

Citations

Citeable URL: https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/nk322f75h

Abstract

Speculative execution attacks leverage a processor’s speculative execution optimization to leak secret information. Previous attempts to generalize transient execution attacks often analyze specific gadgets in software or look solely at microarchitectural state artifacts to explain the fundamental logic behind these attacks. In this work, we present SpecCheck, a systematic security verification for detecting potential transient data leakage. SpecCheck is based on a description of a generic transient execution attack in the form of a register based Finite State Machine (FSM) that is easily incorporated into commonly used processor simulators. SpecCheck’s key insight is the fact that transient execution attacks involve both the software and the hardware to succeed and the only way to verify if a design is capable of mitigating such attacks is by considering both at verification time. As a proof of concept, we implement SpecCheck’s FSM in the gem5 simulator to check for suspicious program flows during an arbitrary program’s simulation and lay the groundwork for a robust and systematic hardware security verification tool. We show that SpecCheck is able to identify known transient execution gadgets in four of the main Spectre variants while incurring on average only a 4% simulation time overhead.

Creator