System-level Non-interference for Constant-time Cryptography

Abstract : Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based en-vironments, where they have been used to recover secret keys from cryptographic implementations. One common ap-proach to thwart cache-based attacks is to use constant-time implementations, i.e. which do not branch on secrets and do not perform memory accesses that depend on secrets. How-ever, there is no rigorous proof that constant-time implemen-tations are protected against concurrent cache-attacks in virtualization platforms with shared cache; moreover, many prominent implementations are not constant-time. An alter-native approach is to rely on system-level mechanisms. One recent such mechanism is stealth memory, which provisions a small amount of private cache for programs to carry po-tentially leaking computations securely. Stealth memory in-duces a weak form of constant-time, called S-constant-time, which encompasses some widely used cryptographic imple-mentations. However, there is no rigorous analysis of stealth memory and S-constant-time, and no tool support for check-ing if applications are S-constant-time. We propose a new information-flow analysis that checks if an x86 application executes in constant-time, or in S-constant-time. Moreover, we prove that constant-time (resp. S-constant-time) programs do not leak confidential infor-mation through the cache to other operating systems exe-cuting concurrently on virtualization platforms (resp. plat-forms supporting stealth memory). The soundness proofs are based on new theorems of independent interest, includ-ing isolation theorems for virtualization platforms (resp. plat-forms supporting stealth memory), and proofs that constant-time implementations (resp. S-constant-time implementa-tions) are non-interfering with respect to a strict information flow policy which disallows that control flow and memory ac-cesses depend on secrets. We formalize our results using the Coq proof assistant and we demonstrate the effectiveness of our analyses on cryptographic implementations, including PolarSSL AES, DES and RC4, SHA256 and Salsa20.
Type de document :
Communication dans un congrès
ACM SIGSAC Conference on Computer and Communications Security, CCS'14, Nov 2014, Scottsdale, United States. ACM, pp.1267 - 1279, 2014, 〈http://www.sigsac.org/ccs/CCS2014/〉. 〈10.1145/2660267.2660283〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01101950
Contributeur : David Pichardie <>
Soumis le : samedi 10 janvier 2015 - 21:03:39
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : lundi 13 avril 2015 - 05:09:03

Fichier

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

Identifiants

Citation

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie. System-level Non-interference for Constant-time Cryptography. ACM SIGSAC Conference on Computer and Communications Security, CCS'14, Nov 2014, Scottsdale, United States. ACM, pp.1267 - 1279, 2014, 〈http://www.sigsac.org/ccs/CCS2014/〉. 〈10.1145/2660267.2660283〉. 〈hal-01101950〉

Partager

Métriques

Consultations de la notice

941

Téléchargements de fichiers

282