Paper 2023/1514 Original: eprint.iacr.org/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)
PDF- Category
- Foundations
- Publication info
- Preprint.
- History
- 2025-01-06: last updated
- 2023-10-04: published
- Short URL
- https://ia.cr/2023/1514
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}