Description
Date depot: 1 janvier 1900
Titre: Preuve formelle de contre-mesures aux attaques sur les implémentations cryptographiques.
Directeur de thèse:
Renaud PACALET (LTCI (EDMH))
Directeur de thèse:
Jean-Luc DANGER (LTCI (EDMH))
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Suite à la publication de la 'timing attack' de Paul C. Kocher en 1996, l'industrie liée à la sécurité numérique s'est mobilisée contre les attaques par canaux auxiliaires. Une vulnérabilité supplémentaire est apparue dès 1997 avec la mise en évidence par Dan Boneh des attaques en injection de faute sur RSA/CRT. Depuis, les attaques dites 'en perturbation' sont considérées comme une menace de premier plan contre les systèmes sensibles, parce que leur efficacité est sans précédent : par exemple, une seule signature erronée permet de casser le cryptosystème RSA/CRT et une ou deux fautes pendant le chiffrement ou la routine de diversification des clés de tours permet de retrouver la clé d'un AES-128. Dans ces deux cas de figure, la faute peut provenir de l'extérieur (comme par exemple une injection laser ou électromagnétique) ou de l'intérieur même du composant (péril popularisé sous le nom de 'bug attack').
Dans ce contexte, il est nécessaire d'implémenter des parades à la fois contre les attaques en observation et en perturbation dans les systèmes critiques. L'objectif de cette thèse est de passer en revue quelques contre-mesures solidement fondées, et de montrer que, pour certaines d'entre elles, leur sécurité escomptée peut être prouvée formellement. Les démonstrations seront deux types : (i) la conformité d'une implémentation par rapport aux spécifications et (ii) l'établissement de la véracité de propriétés de sécurité concernant les attaques physiques en observation et en perturbation. Afin de couvrir une gamme représentative de contre-mesures, le projet de recherche couvrira l'évaluation de deux familles de protections. Tout d'abord une contre-mesure statique aux attaques physiques, à savoir BCDL, qui présente l'avantage de la simplicité. Ensuite une contre-mesure dynamique, à savoir la méthode de la 'fuite chiffrée' (ou 'encrypted leakage'), qui est plus compacte mais qui nécessite une voire deux sources d'aléa, et qui est donc plus délicate à mettre en ½uvre et à prouver.
Doctorant.e: Maghrebi Houssem