Enforcing Fine-grained Constant-time Policies - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Enforcing Fine-grained Constant-time Policies

Résumé

Cryptographic constant-time (CT) is a popular programming discipline used by cryptographic libraries to protect themselves against timing attacks. The CT discipline aims to enforce that program execution does not leak secrets, where leakage is defined by a formal leakage model. In practice, different leakage models coexist, sometimes even within a single library, both to reflect different architectures 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 models 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.

Dates et versions

hal-03844366 , version 1 (08-11-2022)

Identifiants

Citer

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya. Enforcing Fine-grained Constant-time Policies. CCS 2022 - 2022 ACM SIGSAC Conference on Computer and Communications Security, Nov 2022, Los Angeles CA, United States. pp.83-96, ⟨10.1145/3548606.3560689⟩. ⟨hal-03844366⟩
66 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More