Analyse des vulnérabilités des protocoles sur cible matérielle // vulnerability analysis of protocols on hardware devices

Topic description

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 : Information Technology Security Evaluation Facility (ITSEF) conducts activities in the field of security evaluation of electronic systems, embedded software components, either within the framework of certification schemes, for example the one led by the l’Agence Nationale de la Sécurité des Systèmes d’information (ANSSI), or at the direct request of developers.
In the context of security evaluations conducted by the ITSEF, evaluators are required, among other things, to test the resistance of cryptographic mechanisms embedded on smart cards against physical attacks, such as chip tampering attacks or attacks by observing compromising signals. In an application context (banking, healthcare, identity), these mechanisms are used within cryptographic protocols, such as key exchanges or authentications. When a vulnerability is detected in a product, the evaluator must analyze its impact on the protocol. Currently, this analysis relies on the evaluator's expertise, but the use of formal methods would be advantageous for tracing attack paths or for providing greater assurance that the vulnerability will not be exploited.
Initially, this thesis will focus on studying existing verification tools (e.g., Tamarin [1]) in order to test them on the protocols used in commonly evaluated applications. The thesis will then aim to examine the different ways in which a vulnerability can be expressed within the protocol, and to evaluate the tool's ability to formally analyze its impacts by identifying attack paths. Finally, the PhD student will be required to enhance the tool with new components to address the identified needs.
References
[1] Tamarin : fr : Direction de la Recherche Technologique
Pôle en : Technological Research
Département : Département Systèmes (LETI)
Service : Service Sécurité des Systèmes Electroniques et des Composants
Laboratoire : Centre d’Evaluation de la Sécurité des Technologies de l’Information
Date de début souhaitée : 01-09-
Ecole doctorale : Mathématiques, Sciences et Technologies de l’Information, Informatique (MSTII)

Funding category

Public/private mixed funding

Funding further details