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