Paper 2023/1514
Leakage-Free Probabilistic Jasmin Programs
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)
- 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
-
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} }