Leakage-Free Probabilistic Jasmin Programs

José Bacelar Almeida; Denis Firsov; Tiago Oliveira; Dominique Unruh

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: cryptography formal methods EasyCrypt leakage-freeness side-channels timing attack rejection sampling Jasmin
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: 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},
      note = {\url{https://eprint.iacr.org/2023/1514}},
      url = {https://eprint.iacr.org/2023/1514}
}