Paper 2023/1514

Leakage-Free Probabilistic Jasmin Programs

José Bacelar Almeida, Universidade do Minho, Braga, Portugal, INESC TEC, Porto, Portugal
Denis Firsov, Tallinn University of Technology, Guardtime
Tiago Oliveira, Max Planck Institute for Security and Privacy
Dominique Unruh, University of Tartu
Abstract

We give a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization also covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove equivalence of both definitions. We also prove that our new characterizations are compositional. Finally, we relate new definitions to the existing ones from prior work which only apply to deterministic programs. To test our definitions we use Jasmin toolchain to develop a rejection sampling algorithm and prove (in EasyCrypt) that the implementation is leakage-free whilst not being constant-time.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Preprint.
Keywords
cryptographyformal methodsEasyCryptleakage-freenessside-channelstiming attackrejection samplingJasmin
Contact author(s)
jba @ di uminho pt
denis firsov @ gmail com
tiago oliveira @ mpi-sp org
unruh @ ut ee
History
2023-10-06: revised
2023-10-04: received
See all versions
Short URL
https://ia.cr/2023/1514
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/1514,
      author = {José Bacelar Almeida and Denis Firsov and Tiago Oliveira and Dominique Unruh},
      title = {Leakage-Free Probabilistic Jasmin Programs},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/1514},
      year = {2023},
      url = {https://eprint.iacr.org/2023/1514}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.