Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Secure Compilation of Constant-Resource Programs

Abstract : Observational non-interference (ONI) is a generic information-flow policy for side-channel leakage. Informally, a program is ONI-secure if observing program leakage during execution does not reveal any information about secrets. Formally, ONI is parametrized by a leakage function ℓ, and different instances of ONI can be recovered through different instantiations of ℓ. One popular instance of ONI is the cryptographic constant-time (CCT) policy, which is widely used in cryptographic libraries to protect against timing and cache attacks. Informally, a program is CCT-secure if it does not branch on secrets and does not perform secret-dependent memory accesses. Another instance of ONI is the constant-resource (CR) policy, a relaxation of the CCT policy which is used in Amazon's s2n implementation of TLS and in several other security applications. Informally, a program is CR-secure if its cost (modelled by a tick operator over an arbitrary semi-group) does not depend on secrets. In this paper, we consider the problem of preserving ONI by compilation. Prior work on the preservation of the CCT policy develops proof techniques for showing that main compiler optimisations preserve the CCT policy. However, these proof techniques critically rely on the fact that the semi-group used for modelling leakage satisfies the property: ℓ1 + ℓ1' = ℓ2 + ℓ2' ⇒ ℓ1 = ℓ2 ∧ ℓ1' = ℓ2'. Unfortunately, this non-cancelling property fails for the CR policy, because its underlying semi-group is (ℕ,+) and it is currently not known how to extend existing techniques to policies that do not satisfy non-cancellation. We propose a methodology for proving the preservation of the CR policy during a program transformation. We present an implementation of some elementary compiler passes, and apply the methodology to prove the preservation of these passes. Our results have been mechanically verified using the Coq proof assistant
Type de document :
Communication dans un congrès
Liste complète des métadonnées
Contributeur : Rémi Hutin Connectez-vous pour contacter le contributeur
Soumis le : samedi 8 mai 2021 - 17:40:27
Dernière modification le : vendredi 5 août 2022 - 14:54:52
Archivage à long terme le : : lundi 9 août 2021 - 18:14:22


Secure Compilation of Constant...
Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-03221440, version 1


Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie. Secure Compilation of Constant-Resource Programs. CSF 2021 - 34th IEEE Computer Security Foundations Symposium, Jun 2021, Dubrovnik, Croatia. pp.1-12. ⟨hal-03221440⟩



Consultations de la notice


Téléchargements de fichiers