Résumé:
La preuve formelle de primitives cryptographiques révèle plusieurs défis. Le premier est de savoir comment exprimer la sécurité des ces primitives. Cette notion de sécurité devant prendre en compte le fait que la primitive doit résister à des attaquants “arbitraires ». Le second est de montrer que ces primitives vérifient les propriétés de sécurité précédemment définies. Dans un premier temps je montrerai comment ces propriétés peuvent être définies dans l’assistant de preuve EasyCrypt, puis je ferai un tour d’horizon des techniques de preuves qui peuvent être utilisées pour les établir. J’insisterai sur les deux difficultés principales: comment raisonner sur des programmes probabilistes et comment faire des preuves universellement quantifiées pour tous les adversaires. Cette première partie de l’exposé se concentrera sur les preuves de primitives cryptographiques au niveau algorithmique. Dans un deuxième temps j’expliquerai comment nous pouvons obtenir les mêmes garanties de sécurités au niveau des implémentations et en particulier au niveau du code assembleur. Nous verrons aussi comment il est possible d’apporter des garanties supplémentaires sur le code assembleur comme la résistance aux attaques par cache ou aux attaques de type Spectre.
