Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Testing side-channel security of cryptographic implementations against future microarchitectures

Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom

TL;DR

The paper tackles how future microarchitectures could introduce side-channel leaks in cryptographic implementations. It introduces Lm-Spec, a domain-specific language for modeling leakage and speculative execution, and Lm-Test, a framework for automatically detecting secret-dependent leaks via relational testing. Through a large-scale case study of 18 optimizations across 25 cryptographic implementations, the authors show that many real libraries would leak under these future proposals, including leaks arising from coding idioms designed to be constant-time. The work provides a practical, extensible approach for hardware and software designers to evaluate and mitigate microarchitectural leakage risks early in the development cycle.

Abstract

How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size of transistors, chip vendors have started developing new microarchitectural optimizations to speed up computation. A recent study (Sanchez Vicarte et al., ISCA 2021) suggests that these optimizations might open the Pandora's box of microarchitectural attacks. However, there is little guidance on how to evaluate the security impact of future optimization proposals. To help chip vendors explore the impact of microarchitectural optimizations on cryptographic implementations, we develop (i) an expressive domain-specific language, called LmSpec, that allows them to specify the leakage model for the given optimization and (ii) a testing framework, called LmTest, to automatically detect leaks under the specified leakage model within the given implementation. Using this framework, we conduct an empirical study of 18 proposed microarchitectural optimizations on 25 implementations of eight cryptographic primitives in five popular libraries. We find that every implementation would contain secret-dependent leaks, sometimes sufficient to recover a victim's secret key, if these optimizations were realized. Ironically, some leaks are possible only because of coding idioms used to prevent leaks under the standard constant-time model.

Testing side-channel security of cryptographic implementations against future microarchitectures

TL;DR

The paper tackles how future microarchitectures could introduce side-channel leaks in cryptographic implementations. It introduces Lm-Spec, a domain-specific language for modeling leakage and speculative execution, and Lm-Test, a framework for automatically detecting secret-dependent leaks via relational testing. Through a large-scale case study of 18 optimizations across 25 cryptographic implementations, the authors show that many real libraries would leak under these future proposals, including leaks arising from coding idioms designed to be constant-time. The work provides a practical, extensible approach for hardware and software designers to evaluate and mitigate microarchitectural leakage risks early in the development cycle.

Abstract

How will future microarchitectures impact the security of existing cryptographic implementations? As we cannot keep reducing the size of transistors, chip vendors have started developing new microarchitectural optimizations to speed up computation. A recent study (Sanchez Vicarte et al., ISCA 2021) suggests that these optimizations might open the Pandora's box of microarchitectural attacks. However, there is little guidance on how to evaluate the security impact of future optimization proposals. To help chip vendors explore the impact of microarchitectural optimizations on cryptographic implementations, we develop (i) an expressive domain-specific language, called LmSpec, that allows them to specify the leakage model for the given optimization and (ii) a testing framework, called LmTest, to automatically detect leaks under the specified leakage model within the given implementation. Using this framework, we conduct an empirical study of 18 proposed microarchitectural optimizations on 25 implementations of eight cryptographic primitives in five popular libraries. We find that every implementation would contain secret-dependent leaks, sometimes sufficient to recover a victim's secret key, if these optimizations were realized. Ironically, some leaks are possible only because of coding idioms used to prevent leaks under the standard constant-time model.
Paper Structure (54 sections, 6 figures, 1 table, 1 algorithm)

This paper contains 54 sections, 6 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Overview
  3. Modeling leaks with Lm-Spec
  4. Modeling speculation with Lm-Spec
  5. Generating leakage traces
  6. Specifying side-channel security
  7. Detecting leaks with Lm-Test
  8. Modeling leakage in Lm-Spec
  9. The Lm-Spec language
  10. Silent store suppression
  11. Register file compression
  12. Computation reuse
  13. Modeling speculation in Lm-Spec
  14. Prediction clauses in Lm-Spec
  15. Control-flow speculation
  16. ...and 39 more sections

Figures (6)

  • Figure 1: Modeling constant-time requirements in Lm-Spec
  • Figure 2: Modeling branch speculation in Lm-Spec
  • Figure 3: Diagram showing Lm-Test's internal workflow. A user provides as input a leakage clause and possibly a prediction clause, as well as the program to test. The labeled interface specifies the format of inputs and which inputs are secret.
  • Figure 4: Syntax of Lm-Spec. Words and symbols in fixed-width are verbatim keywords, words in italics are syntactic forms either of Hy or defined here, and names with underwave can be replaced by any valid identifier. Syntactic groups with a [0pt][-1.5pt] square hat are either optional? or repeatable*.
  • Figure 5: Lm-Spec's context variables
  • ...and 1 more figures