Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Efficient Verification of Constant-Time Cryptographic Implementations

Luwei Cai, Fu Song, Taolue Chen

TL;DR

This paper tackles the challenge of verifying constant-time cryptographic implementations against timing side-channel leaks. It introduces CT-Prover, a practical verification tool that fuses a lightweight IFDS-based taint analysis with a precise taint analysis built on taint-directed semi-cross-products and taint-directed self-composition to achieve scalable, sound verification on production LLVM IR code. The approach proves 72 of 87 real-world benchmarks constant-time, while identifying new vulnerabilities in libraries like Mbed TLS and BearSSL, and significantly outperforms the state-of-the-art ct-verif in many cases. Its hybrid strategy—combining fast, broad tainting with targeted, rigorous safety checks—demonstrates that heavy verification can be made viable at industry scale, offering a concrete path toward automated, robust constant-time verification for cryptographic software.

Abstract

Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software security. Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks, but developing constant-time implementations turns out to be challenging and error-prone. Current verification approaches/tools suffer from scalability and precision issues when applied to production software in practice. In this paper, we put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Specifically, we first use an IFDS-based lightweight taint analysis to prove that a large number of potential (timing) side-channel sources do not actually leak secrets. We then resort to a precise taint analysis and a safety verification approach to determine whether the remaining potential side-channel sources can actually leak secrets. These include novel constructions of taint-directed semi-cross-product of the original program and its Boolean abstraction, and a taint-directed self-composition of the program. Our approach is implemented as a cross-platform and fully automated tool CT-Prover. The experiments confirm its efficiency and effectiveness in verifying real-world benchmarks from modern cryptographic and SSL/TLS libraries. In particular, CT-Prover identify new, confirmed vulnerabilities of open-source SSL libraries (e.g., Mbed SSL, BearSSL) and significantly outperforms the state-of-the-art tools.

Towards Efficient Verification of Constant-Time Cryptographic Implementations

TL;DR

This paper tackles the challenge of verifying constant-time cryptographic implementations against timing side-channel leaks. It introduces CT-Prover, a practical verification tool that fuses a lightweight IFDS-based taint analysis with a precise taint analysis built on taint-directed semi-cross-products and taint-directed self-composition to achieve scalable, sound verification on production LLVM IR code. The approach proves 72 of 87 real-world benchmarks constant-time, while identifying new vulnerabilities in libraries like Mbed TLS and BearSSL, and significantly outperforms the state-of-the-art ct-verif in many cases. Its hybrid strategy—combining fast, broad tainting with targeted, rigorous safety checks—demonstrates that heavy verification can be made viable at industry scale, offering a concrete path toward automated, robust constant-time verification for cryptographic software.

Abstract

Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software security. Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks, but developing constant-time implementations turns out to be challenging and error-prone. Current verification approaches/tools suffer from scalability and precision issues when applied to production software in practice. In this paper, we put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Specifically, we first use an IFDS-based lightweight taint analysis to prove that a large number of potential (timing) side-channel sources do not actually leak secrets. We then resort to a precise taint analysis and a safety verification approach to determine whether the remaining potential side-channel sources can actually leak secrets. These include novel constructions of taint-directed semi-cross-product of the original program and its Boolean abstraction, and a taint-directed self-composition of the program. Our approach is implemented as a cross-platform and fully automated tool CT-Prover. The experiments confirm its efficiency and effectiveness in verifying real-world benchmarks from modern cryptographic and SSL/TLS libraries. In particular, CT-Prover identify new, confirmed vulnerabilities of open-source SSL libraries (e.g., Mbed SSL, BearSSL) and significantly outperforms the state-of-the-art tools.
Paper Structure (17 sections, 4 theorems, 5 equations, 9 figures, 3 tables)

This paper contains 17 sections, 4 theorems, 5 equations, 9 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The While Language
  4. Constant-Time Security
  5. Motivation and Overview
  6. Motivating Examples
  7. Approach Overview
  8. Methodology
  9. Lightweight Taint Analysis
  10. Precise Taint Analysis via Taint-directed Semi-cross-product
  11. Taint-directed Self-composition
  12. Implementation and Evaluation
  13. Verifying Constant-time Implementations (RQ1, RQ3)
  14. Verifying Non-constant-time Implementations (RQ2, RQ3)
  15. Threats to Validity
  16. ...and 2 more sections

Key Result

lemma 1

For any potential side-channel source $(\ell,x)$ and pair $(c_0,c_0')$ of initial configurations such that $(c_0\simeq_{\mathbb{X}^{in}_l} c_0')$, if $x$ is not tainted at the label $\ell$, i.e., $x\not\in T_\ell$, then the values of $x$ are the same at the label $\ell$ in any pair of complete execu

Figures (9)

  • Figure 1: The syntax of While.
  • Figure 2: The operational semantics of the While program.
  • Figure 3: Fragment of the function fixfrac taken from the libfixedtimefixedpoint library.
  • Figure 4: Simplified fragment of the function crypto_stream_chacha20_ref taken from the libsodium library.
  • Figure 5: Overview of our approach
  • ...and 4 more figures

Theorems & Definitions (6)

  • definition 1: Constant-time Leakage Model
  • definition 2: Constant-time Security ABBDE16
  • lemma 1
  • lemma 2
  • lemma 3
  • theorem 1