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, Input Output
Tiago Oliveira, SandboxAQ
Dominique Unruh, University of Tartu, RWTH Aachen University
Abstract

This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Minor revision. ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '25)
DOI
10.1145/3703595.3705871
Keywords
cryptographyformal methodsEasyCryptleakage-freenessside-channelstiming attackrejection samplingJasmin
Contact author(s)
jba @ di uminho pt
denis firsov @ taltech ee
tiago oliveira @ sandboxquantum com
leakage k31fea @ rwth unruh de
History
2025-01-06: last of 2 revisions
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},
      doi = {10.1145/3703595.3705871},
      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.