Welcome to the resource topic for 2022/630
Title:
Enforcing fine-grained constant-time policies
Authors: Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, 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.
ePrint: https://eprint.iacr.org/2022/630
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .