SpecSafe: Detecting Cache Side Channels in a Speculative World

The high-profile Spectre attack and its variants have revealed that speculative execution may leave secret- dependent footprints in the cache, allowing an attacker to learn confidential data. However, existing static side-channel detectors either ignore speculative execution, leading to false negatives, or lack a precise cache model, leading to false positives. In this paper, somewhat surprisingly, we show that it is challenging to develop a speculation-aware static analysis with precise cache models: a combination of existing works does not necessarily catch all cache side channels. Motivated by this observation, we present a new semantic definition of security against cache-based side-channel attacks, called Speculative-Aware noninterference (SANI), which is applicable to a variety of attacks and cache models. We also develop SpecSafe to detect the violations of SANI. Unlike other speculation-aware symbolic executors, SpecSafe employs a novel program transformation so that SANI can be soundly checked by speculation-unaware side-channel detectors. SpecSafe is shown to be both scalable and accurate on a set of moderately sized benchmarks, including commonly used cryptography libraries.

Files

Metadata

Work Title SpecSafe: Detecting Cache Side Channels in a Speculative World
Subtitle Proceedings of Object-Oriented Programming, Systems, Languages & Applications Conference (OOPSLA)
Access
Open Access
Creators
  1. Robert Brotzman-Smith
  2. Danfeng Zhang
  3. G Tan
  4. M T Kandemir
License In Copyright (Rights Reserved)
Work Type Article
Publication Date January 1, 2021
Deposited September 27, 2022

Versions

Analytics

Collections

This resource is currently not in any collection.

Work History

Version 1
published

  • Created
  • Added oopsla21.pdf
  • Added Creator Robert Brotzman-Smith
  • Added Creator Danfeng Zhang
  • Added Creator G Tan
  • Added Creator M T Kandemir
  • Published
  • Updated