Yuheng Yang*, Qinhan Tan*, Thomas Bourgeat, Sharad Malik, Mengjia Yan
Abstract:
Hardware information flow tracking (IFT) using taint analysis provides a methodology to check whether a hardware design satisfies certain security properties.
Previous work has... shown a broad trade-off space between precision and complexity when using different taint analysis schemes.
A careful investigation of this space has led to the insight that applying different taint schemes to different components of a hardware design can improve overall efficiency.
We present Compass, a systematic framework to guide users in designing appropriate taint schemes that are as lightweight as possible while still sufficient to accomplish their security verification goals. We first establish a unified terminology to comprehensively capture existing taint schemes. We then apply counterexample-guided abstraction refinement (CEGAR) for taint refinement to iteratively improve the taint scheme. We evaluated Compass on a set of open-source RISCV processors to verify the information flow properties for speculative execution vulnerabilities, and demonstrate that Compass significantly improves both simulation speed and formal-verification scalability of taint analysis. Extend
Qinhan Tan*, Yuheng Yang*, Thomas Bourgeat, Sharad Malik, Mengjia Yan
Yuheng Yang, Thomas Bourgeat, Stella Lau, Mengjia Yan
MIT EECS William A. Martin Master Thesis Award,
Best Poster Award (NEHWS Workshop)
ISCA Lightning,
Code,
Slide (ISCA, Intel RARE Workshop, FCCM Workshop, NEHWS Workshop),
Poster
Abstract:
Traditional modeling approaches in computer architecture aim to obtain an accurate estimation of performance, area, and energy of a processor design.
With the advent of speculative execution attacks and... their security concerns, these traditional modeling techniques fall short when used for security evaluation of defenses against these attacks.
This paper presents Pensieve, a security evaluation framework targeting early-stage microarchitectural defenses against speculative execution attacks. At the core, it introduces a modeling discipline for systematically studying early-stage defenses. This discipline allows us to cover a space of designs that are functionally equivalent while precisely capturing timing variations due to resource contention and microarchitectural optimizations. We implement a model checking framework to automatically find vulnerabilities in designs. We use Pensieve to evaluate a series of state-of-the-art invisible speculation defense schemes, including Delay-on-Miss, InvisiSpec, and GhostMinion, against a formally defined security property, speculative non-interference. Pensieve finds Spectre-like attacks in all those defenses, including a new speculative interference attack variant that breaks GhostMinion, one of the latest defenses. Extend
Peter W. Deutsch*, Yuheng Yang*, Thomas Bourgeat, Jules Drean, Joel Emer, Mengjia Yan
ASPLOS,
Slide (ASPLOS),
Poster
Thomas Bourgeat*, Jules Drean*, Yuheng Yang, Lillian Tsai, Joel Emer, Mengjia Yan
Intel Hardware Security Academic Award 2022 Finalist,
Top Picks Honorable Mention (Top Picks Workshop at ICCAD)
Slide (Top Picks Workshop at ICCAD)