Paper 2022/630
Enforcing fine-grained constant-time policies
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya
Abstract
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.
Metadata
- 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 - History
- 2022-05-23: received
- Short URL
- https://ia.cr/2022/630
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2022/630, 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}, url = {https://eprint.iacr.org/2022/630} }