Leakage-Free Probabilistic Jasmin Programs

RWTH Publications (RWTH Aachen)

Abstract

This paper presents a semantic characterization of leakagefreeness 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.

Authors 4

1. José Bacelar Almeida
2. Denis Firsov
3. Tiago Ribeiro De Oliveira
4. Dominique Unruh Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen