Tamarin cherche les failles dans les protocoles
18 juin 2022
Nos vies numériques sont régies par un grand nombre de protocoles informatiques qui garantissent la sécurité des échanges de données, comme le standard EMV (European Mastercard Visa) pour les transactions bancaires ou le protocole TLS (Transport Layer Security) qui assure la sécurisation des échanges sur Internet. Jannik Dreier, enseignant-chercheur à Telecom Nancy et à l’Université de Lorraine, membre de l’équipe PESTO, commune à Inria et au Loria, travaille à débusquer les failles de ces protocoles. Il avance dans ces labyrinthes cryptographiques avec un outil précieux : le logiciel Tamarin.
Aller plus vite et faire moins d’erreurs
En 2021, des chercheurs de l’ETH (Eidgenössische Technische Hochschule, École polytechnique fédérale en Français) de Zurich ont repéré une faille dans le réseau EMV (Europay Mastercard et Visa), standard international des échanges par carte bancaire. Une faiblesse de ce vaste protocole facilite en effet des attaques sur les terminaux de paiement en leur faisant croire qu’il n’y a pas de limitation au paiement sans contact pour les cartes bancaires. La faille a été découverte grâce à Tamarin, un logiciel développé depuis 2012 par des scientifiques de l’ETH, du CISPA(Center for IT-Security, Privacy and Accountability, Centre pour la sécurité, la confidentialité et la responsabilité en matière de sécurité informatique) de Sarrebruck, de l’Université d’Oxford et de l’Université de Lorraine. Jannik Dreier fait partie de l’équipe de développeurs assurant la maintenance de ce logiciel open source.
« La demande d’analyse de protocoles est en constante augmentation, en particulier dans les moments de standardisation, comme avec le protocole de la 5G récemment. L’objectif de Tamarin, ou de ProVerif, un autre logiciel développé par Inria, est de faire moins d’erreurs. » Pour trouver des erreurs, les spécialistes de la vérification formelle de protocoles cryptographiques comme Jannik Dreier analysent les documents de spécification, des documents techniques utilisés par les développeurs pour produire du code, puis créent des modèles mathématiques pour vérifier la sécurité du protocole en présence d’un attaquant : que se passerait-il si… ? « C’est un long travail d’analyse, fait « à la main », commente le chercheur.
Automatiser et rendre accessible le travail de vérification
En 2012, le lancement de Tamarin répond au besoin d’un outil pour automatiser cette étape d’analyse. Pour Jannik Dreier : « L’originalité de Tamarin est de pouvoir faire une modélisation très précise de la cryptographie d’un protocole et de ses faiblesses. Le logiciel aide à trouver des failles mais aussi à faire ensuite des choix dans la correction du protocole. On peut tester ces différents choix, sans augmenter les coûts en temps de travail. »
L’outil est utilisé aujourd’hui par la communauté scientifique et, de plus en plus, par des industriels. « Depuis 2012, il est constamment amélioré avec l’aide d’une large communauté d’utilisateurs, dans le but de le rendre plus automatique et plus facilement utilisable pour des non-experts. C’est très plaisant à constater », reconnaît Jannik Dreier qui anime en équipe ce projet depuis plusieurs années. Tamarin sort du cadre universitaire et continue de débusquer les failles de sécurité. Récemment, c’est avec lui qu’a été identifiée une faille dans le protocole de la 5G.
Plus d’informations :
