Affordable Access

Secure Compilation of Constant-Resource Programs

Authors
  • Barthe, Gilles
  • Blazy, Sandrine
  • Hutin, Rémi
  • Pichardie, David
Publication Date
Jun 21, 2021
Source
HAL-INRIA
Keywords
Language
English
License
Unknown
External links

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:

Report this publication

Statistics

Seen <100 times