Verifying Constant-Time Implementations by Abstract Interpretation

Sandrine Blazy 1 David Pichardie 1 Alix Trieu 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Constant-time programming is an established discipline to secure programs against timing attacks. 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 evidences 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.
Type de document :
Communication dans un congrès
European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway. 22nd European Symposium on Research in Computer Security
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01588444
Contributeur : Alix Trieu <>
Soumis le : vendredi 15 septembre 2017 - 16:28:19
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14
Document(s) archivé(s) le : samedi 16 décembre 2017 - 14:29:27

Fichier

esorics17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01588444, version 1

Citation

Sandrine Blazy, David Pichardie, Alix Trieu. Verifying Constant-Time Implementations by Abstract Interpretation. European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway. 22nd European Symposium on Research in Computer Security. 〈hal-01588444〉

Partager

Métriques

Consultations de la notice

203

Téléchargements de fichiers

24