Vous êtes ici : UVSQ RechercheDoctoratSoutenances de thèse

«Preuves de sécurité outillées d'implémentations cryptographiques» par Maria Christofi

Présentée par : Maria Christofi Discipline : informatique Laboratoire : PRISM

Résumé :
Dans cette thèse, nous nous sommes intéressés à la vérification formelle des implémentations cryptographiques. Dans la première partie, nous étudions la vérification du protocole mERA à l’aide d’outil ProVerif. Nous vérifions que ce protocole assure certaines propriétés de sécurité, notamment l’authentification, le secret et la non-reliabilité, ainsi que des propriétés comme la vivacité du protocole. Dans la deuxième partie de cette thèse, nous étudions la vérification formelle des implémentations cryptographiques vis-à-vis d’un certain type d’attaque: les attaques par injection de faute modifiant les données. Nous identifions et présentons les différents modèles de ce type d’attaque en tenant en compte plusieurs paramètres. Ensuite, nous modélisons des implémentations cryptographiques (munies de contremesures), nous injectons tous les scenarios de fautes possibles et finalement nous vérifions le code correspondant à l’aide d’outil Frama-C, basé sur l’analyse statique. Nous présentons une application de notre méthode : la vérification d’une implémentation RSA-CRT munie de la contremesure de Vigilant (CHES 2008). Après avoir exprimé les propriétés nécessaires pour la vérification, nous injectons tous les scenarios de fautes possibles (en tenant compte d’un modèle de faute choisi). Cette vérification révèle deux scenarios de fautes provoquant deux attaques susceptibles à fuir des informations secrètes. Afin de mécaniser la vérification, nous avons réussi à automatiser complètement l’insertion des fautes selon les différents modèles (en tenant en compte les attaques mono-fautes, ainsi que les multi-fautes). Ceci a donné naissance à un nouveau plug-in de Frama-C : TL_FACE.

Abstract :
In this thesis, we are interested on the formal verification of cryptographic implementations. In the first part, we study the verification of the protocol mERA using the tool ProVerif. We prove that this protocol verifies some security properties, like the authentication, the secrecy and the unlinkability, but also properties like its vivacity. In the second part of this thesis, we study the formal verification of cryptographic implementations against an attack family: attacks with fault injection modifying data. We identify and present the different models of these attacks considering different parameters. We then model the cryptographic implementation (with its countermeasures), we inject all possible fault scenarios and finally we verify the corresponding code using the Frama-C tool, based on static analysis techniques. We present a use case of our method: the verification of an CRT-RSA implementation with Vigilant’s countermeasure. After expressing the necessary properties for the verification, we inject all fault scenarios (regarding the chosen fault model). This verification reveals two fault scenarios susceptible to flow secret information. In order to mechanize the verification, we insert fault scenarios automatically according to both single and multi fault attacks). This creates a new Frama-C plug-in: TL-FACE.

Informations complémentaires
Jean-Louis LANET, Professeur des Universités, à l’Université de Limoges/Laboratoire XLIM - Limoges - Rapporteur
Graham STEEL, Chargé de Recherche, Habilité à Diriger des Recherches, à l’INRIA/Laboratoire LSV - Cachan - Rapporteur
Louis GOUBIN, Professeur des Universités, à l’Université de Versailles Saint-Quentin-en-Yvelines/Laboratoire Parallélisme, Réseaux, Système, Modélisation (PRISM) - Versailles - Directeur de thèse
Boutheina CHETALI, Chargée de Recherche, à Trusted Labs - Versailles - Examinateur
Loïc CORRENSON, Chercheur, au CEA - Centre de Saclay - Gif/Yvette - Examinateur
Jean-Luc DANGER, Directeur d’Etudes, à Télécom ParisTech - Paris - Examinateur
David NACCACHE, Professeur des Universités, à l’ENS - Cachan - Examinateur
Pascal PAILLIER, Ingénieur de Recherche à Cryptoexperts - Paris - Examinateur
Contact :
dredval service FED :