Paper 2022/630

Enforcing fine-grained constant-time policies

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya


Cryptographic constant-time (CT) is a popular programming disci- pline used by cryptographic libraries to protect themselves against timing attacks. The CT discipline aims to enforce that program ex- ecution does not leak secrets, where leakage is defined by a formal leakage model. In practice, different leakage models coexist, some- times even within a single library, both to reflect different architec- tures and to accommodate different security-efficiency trade-offs. Constant-timeness is popular and can be checked automatically by many tools. However, most sound tools are focused on a baseline (BL) leakage model. In contrast, (sound) verification methods for other leakage models are less developed, in part because these mod- els require modular arithmetic reasoning. In this paper, we develop a systematic, sound, approach for enforcing fine-grained constant- time policies beyond the BL model. Our approach combines two main ingredients: a verification infrastructure, which proves that source programs are constant-time, and a compiler infrastructure, which provably preserves constant-timeness for these fine-grained policies. By making these infrastructures parametric in the leakage model, we achieve the first approach that supports fine-grained constant-time policies. We implement the approach in the Jasmin framework for high-assurance cryptography, and we evaluate our approach with examples from the literature: OpenSSL and wolfSSL. We found a bug in OpenSSL and provided a formally verified fix.

Available format(s)
Publication info
Preprint. MINOR revision.
Contact author(s)
basavesh shivakumar @ mpi-sp org
gbarthe @ mpi-sp org
benjamin gregoire @ inria fr
vincent laporte @ inria fr
swarn priya @ inria fr
2022-05-23: received
Short URL
Creative Commons Attribution


      author = {Basavesh Ammanaghatta Shivakumar and Gilles Barthe and Benjamin Grégoire and Vincent Laporte and Swarn Priya},
      title = {Enforcing fine-grained constant-time policies},
      howpublished = {Cryptology ePrint Archive, Paper 2022/630},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.