Psst! Pablo soutient sa thèse ☺

Je suis Pablo Rauzy. Ma thèse s'intitule « Méthodes logicielles formelles pour la sécurité des implémentations cryptographiques ». C'est le résultat de trois ans de recherche supervisée par Sylvain Guilley dans l'équipe sécurité électronique numérique à Télécom ParisTech.

Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités physiques sont exploitées. Mon second objectif est la preuve et l'automatisation des techniques de protection elles-même, car l'écriture manuelle de code est sujette à de nombreuses erreurs, particulièrement lorsqu'il s'agit de code de sécurité.

Les attaques physiques peuvent être classifiées en deux catégories distinctes. Les attaques passives, où l'attaquant peut seulement lire l'information qui fuit par canaux auxiliaires (comme la consommation de courant ou les émanations électromagnétiques). Et les attaques actives, où l'attaquant perturbe le système pour faire en sorte de lui faire révéler des secrets via sa sortie standard. Par conséquent, j'ai poursuivi mes objectifs dans ces deux cadres : sur une contre-mesure qui diminue les fuites par canaux auxiliaires, et sur des contre-mesures contre les attaques par injection de faute.

Comme il existe déjà des propriétés rigoureuses de sécurité pour les protections contre les fuites par canaux auxiliaires, mes contributions se concentrent sur les méthodes formelles pour la conception et la vérification d'implémentations d'algorithmes protégés. J'ai développé une méthode de protection qui, étant donné une implémentation, en génère une version améliorée qui a un rapport signal à bruit nul sur ses canaux auxiliaires, grâce au fait que la fuite a été rendue constante (en particulier, la fuite de dépend pas des données sensibles). Dans l'intérêt de la démonstration, j'ai aussi entrepris d'écrire un outil qui automatise l'application de cette méthode sur un code non sécurisé écrit en langage assembleur. Indépendemment, l'outil permet de prouver que la propriété de fuite constante se vérifie pour une implémentation donnée, ce qui permet de vérifier systématiquement le résultat de la méthode de protection. À ma connaissance, paioli est le premier outil permettant de protéger automatiquement une implémentation contre les fuites par canaux auxiliaires en équilibrant sa fuite de manière prouvable.

À l'inverse, la définition même des objectifs de sécurité n'était pas clairement établie pour les attaques par injection de faute lorsque j'ai commencé ma thèse. Les propriétés de sécurité à prouver n'ayant même pas été formellement énoncées, beaucoup de contre-mesures ont été publiées sans preuve. C'est seulement lors de ma thèse que les « conditions de succès d'attaque » ont été introduites.

En conséquence, la première question a été d'évaluer les contre-mesures existantes par rapport à ces conditions de succès d'attaque. À cette fin, j'ai développé un cadre théorique de travail et un outil qui l'implémente. L'utilisation de finja m'a permis (ainsi qu'à d'autres chercheur·e·s) de vérifier certaines contre-mesures, de retrouver des attaques connues et aussi d'en découvrir de nouvelles.

La seconde question portait sur la minimalité des contre-mesures. J'ai étudié en profondeur l'une des contre-mesures de l'état de l'art. Le résultat de cette étude formelle a été la simplification drastique de la contre-mesure, aussi bien au niveau de la longueur du code que de la nécessité de nombres aléatoires (qui sont coûteux à générer), et ce sans affecter ses propriétés de sécurité. Ce travail a montré la valeur ajoutée des méthodes formelles par rapport à l'ingénierie par essais-erreurs qui a été jusqu'à présent la méthode principale de développement de contre-mesures.

Les contre-mesures existantes revendiquent de protéger contre une ou parfois deux fautes. Cependant, des attaques utilisant plus de deux fautes ont vu le jour, aussi bien en pratique qu'en théorie. La troisième question était alors de concevoir une nouvelle contre-mesure d'ordre supérieur, capable de résister à un nombre arbitraire de fautes. À son tour, la conception d'une nouvelle contre-mesure soulève la question de ce qui fait réellement fonctionner une contre-mesure. Pour tenter de répondre à cette question, j'ai classifié les contre-mesures existantes en essayant d'extraire les principes de protection des techniques employées. Ce travail de catégorisation m'a permis de comprendre l'essence d'une contre-mesure, et, en me basant dessus, de proposer une recette de conception de contre-mesure pouvant résister à un nombre arbitraire (mais fixé) de fautes.

J'ai aussi remarqué que toutes les contre-mesures que j'ai étudiées sont des variantes d'optimisation d'une même technique de base qui consiste à vérifier l'intégrité du calcul en utilisant une forme de redondance. Cette technique est indépendante de l'algorithme auquel elle s'applique, et aussi de la condition de succès d'attaque, puisqu'elle repose entièrement sur des propriétés des structures mathématiques dans lesquelles se trouve les données sensibles, c'est à dire l'arithmétique modulaire. J'ai donc proposé une propriété de résistance face aux attaques par injection de faute qui dépasse la notion de condition de succès d'attaque. La quatrième question a été d'appliquer cette technique de protection à tous les calculs de cryptographie asymétrique, puisqu'ils travaillent tous sur des données mathématiques similairement structurées. Dans cette optique, j'ai développé une abstraction des calculs de cryptographie asymétrique qui permet d'appliquer simplement la méthode de protection par redondance. J'ai formellement défini cette méthode en définissant une transformation de code par réécriture que j'ai prouvée correcte. J'ai écrit un compilateur qui automatise cette transformation et a permis d'obtenir des implémentations protégées d'algorithmes pour lesquels aucune contre-mesure n'a été publiées mais qui sont déjà victimes de nombreuses attaques en faute. Un avantage additionnel du compilateur enredo est de permettre d'étudier le compromis entre sécurité et temps de calcul.

La cérémonie académique débutera à 10h30 en salle Henri Cartan (≈ 70 places).

Pablo présentera son travail lors d'un exposé de quarante-cinq minutes devant les membres du jury et les personnes présentes. Cet exposé sera suivi d'une séance de questions du jury pouvant durer environ une heure.

La cérémonie grotesque (au sens de grotas, cérémonie aussi connue sous le nom de « pot de thèse ») se tiendra ensuite à partir de 12h30 en cour Pasteur, ou dans le passage protégé entre la cour Pasteur et la cour du NIR en cas de pluie.

Un vin d'honneur sera servi, puis un buffet/picnic sera proposé. Il devrait y en avoir pour tous les goûts. Il est tout à fait acceptable de ne venir qu'à la cérémonie grotesque.

→ Si vous souhaitez venir assister à la soutenance et/ou participer au pot de thèse, merci de me confirmer votre présence en m'envoyant un email à <confirmation@pablosoutientsathese.xyz>.

L'ENS se situe au 45 rue d'Ulm, dans le 5ème arrondissement de Paris. Pour vous y rendre :

Bus

Lignes 21 ou 27 Feuillantine.
Ligne 38 Auguste Comte.

Métro

Ligne 10 Cardinal Lemoine.
Ligne 7 Place Monge.

RER

Ligne B Luxembourg.

Une fois à l'ENS le lieu de la soutenance sera fléché.