Leakage-Free Probabilistic Jasmin Programs

Le résumé fourni par la source

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.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.