Verifying constant-time implementations by abstract interpretation - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Article Dans Une Revue Journal of Computer Security Année : 2019

Verifying constant-time implementations by abstract interpretation

Résumé

Constant-time programming is an established discipline to secure programs against timing attackers. Several real-world secure C libraries such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We propose an advanced static analysis, based on state-of-the-art techniques from abstract interpretation, to report time leakage during programming. To that purpose, we analyze source C programs and use full context-sensitive and arithmetic-aware alias analyses to track the tainted flows.We give semantic evidence of the correctness of our approach on a core language. We also present a prototype implementation for C programs that is based on the CompCert compiler toolchain and its companion Verasco static analyzer. We present verification results on various real-world constant-time programs and report on a successful verification of a challenging SHA-256 implementation that was out of scope of previous tool-assisted approaches.
Fichier principal
Vignette du fichier
jcs19.pdf (764.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02025047 , version 1 (17-05-2021)

Identifiants

Citer

Sandrine Blazy, David Pichardie, Alix Trieu. Verifying constant-time implementations by abstract interpretation. Journal of Computer Security, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩. ⟨hal-02025047⟩
124 Consultations
336 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More