Leakage-Free Probabilistic Jasmin Programs

ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 3–16

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.

Authors 4

1. José Bacelar Almeida

   University of Minho

   Affiliation as printed

   HASLAB/INESCTEC, Braga, Portugal

   University of Minho, Braga, Portugal

2. Denis Firsov

   Tallinn University of Technology

   Affiliation as printed

   Input Output, Tallinn, Estonia

   Tallinn University of Technology, Tallinn, Estonia

3. Tiago Oliveira

   SandboxAQ

   Affiliation as printed

   SandboxAQ, Palo Alto, USA

4. Dominique Unruh Aachen

   University of Tartu · RWTH Aachen University

   Affiliation as printed

   RWTH Aachen, Aachen, Germany

   University of Tartu, Tartu, Estonia