Le Centre d’Évaluation de la Sécurité des Technologies de l’Information (CESTI) mène des activités dans le domaine de l’évaluation sécuritaire de systèmes électroniques, de composants de logiciels embarqués, soit dans le cadre de schémas de certification, par exemple celui piloté par l’Agence Nationale de la Sécurité des Systèmes d’information (ANSSI), soit à la demande directe d’industriels.
Dans le contexte des évaluations sécuritaires effectuées par le CESTI, les évaluateurs sont, entre autres, amenés à tester la résistance des mécanismes cryptographiques embarqués sur une carte à puce face aux attaques physiques, comme par exemple les attaques par perturbation de la puce ou les attaques par observation des signaux compromettants. Dans un contexte applicatif (bancaire, santé, identité), ces mécanismes sont employés au sein de protocoles cryptographiques, tels que des échanges de clés ou des authentifications. Lorsqu’une vulnérabilité est détectée sur un produit, l’évaluateur doit analyser les impacts sur le protocole. Aujourd’hui cette analyse repose sur l’expertise de l’évaluateur, mais l’utilisation de méthodes formelles serait un avantage pour la recherche de chemin d’attaque ou pour garantir une meilleure assurance quant à l’absence d’exploitation de la vulnérabilité.
Dans un premier temps, cette thèse consistera à étudier les outils de vérification existants (par exemple Tamarin [1]) afin de les tester sur les protocoles utilisés dans les applications couramment évaluées. L’objectif de la thèse sera ensuite d’examiner les différents moyens pour exprimer une vulnérabilité au sein du protocole, d’évaluer la capacité de l’outil à analyser formellement ses impacts en identifiant des chemins d’attaque. Finalement, le doctorant sera amené à compléter l’outil à l’aide de nouvelles briques pour répondre aux besoins identifiés.
Références
[1] Tamarin : https://github.com/tamarin-prover/tamarin-prover