Leakage-Free Probabilistic Jasmin Programs

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.