### Structured Leakage and Applications to Cryptographic Constant-Time and Cost

Gilles Barthe, Benjamin Gregoire, Vincent Laporte, and Swarn Priya

##### Abstract

Many security properties of interest are captured by instrumented semantics that model the functional behavior and the leakage of programs. For several important properties, including cryptographic constant-time (CCT), leakage models are sufficiently abstract that one can define instrumented semantics for high-level and low-level programs. One important goal is then to relate leakage of source programs and leakage of their compilation---this can be used, e.g.\, to prove preservation of CCT. To simplify this task, we put forward the idea of structured leakage. In contrast to the usual modeling of leakage as a sequence of observations, structured leakage is tightly coupled with the operational semantics of programs. This coupling greatly simplifies the definition of leakage transformers that map the leakage of source programs to leakage of their compilation and yields more precise statements about the preservation of security properties. We illustrate our methods on the Jasmin compiler and prove preservation results for two policies of interest: CCT and cost.

Available format(s)
Category
Foundations
Publication info
Preprint. Minor revision.
Keywords
Secure CompilationCryptographic Constant-TimeCost
Contact author(s)
gjbarthe @ gmail com
benjamin gregoire @ inria fr
vincent laporte @ inria fr
swarn priya @ inria fr
History
2021-05-21: revised
See all versions
Short URL
https://ia.cr/2021/650

CC BY

BibTeX

@misc{cryptoeprint:2021/650,
author = {Gilles Barthe and Benjamin Gregoire and Vincent Laporte and Swarn Priya},
title = {Structured Leakage and Applications to Cryptographic Constant-Time and Cost},
howpublished = {Cryptology ePrint Archive, Paper 2021/650},
year = {2021},
note = {\url{https://eprint.iacr.org/2021/650}},
url = {https://eprint.iacr.org/2021/650}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.