Une équipe de scientifiques passe à la loupe les protocoles cryptographiques
Plutôt que de réparer incessamment des failles de sécurité une fois qu’elles ont été exploitées par un attaquant, il est possible de réduire ces risques en aidant les cryptographes à les détecter en amont grâce à des outils de vérification de protocoles. C’est l’objet des recherches en cybersécurité d'une équipe de scientifiques de l’Institut de recherche en informatique et systèmes aléatoires (IRISA, CNRS/Université de Rennes 1) dont les travaux ont été récompensés par un Distinguished Paper Award lors de la conférence CSF 2022.
Payer en ligne, voter électroniquement, transmettre ses données de santé à la pharmacie. Si ces actions sont protégées, c’est grâce à des protocoles cryptographiques. Ces petits programmes informatiques sécurisent les échanges d’informations. Ils reposent, pour cela, sur des combinaisons d’algorithmes de base tels que le chiffrement et les signatures. Il existe une multitude de protocoles qui évoluent en permanence selon les applications et les ressources des technologies utilisées. Par exemple, un téléphone portable n’offre pas les mêmes capacités qu’une carte à puce. Mais bien qu’ils soient omniprésents dans notre quotidien, sont-ils pour autant infaillibles ? En réalité, des attaques exploitent fréquemment des failles décelées au sein de ces programmes. Elles sont corrigées, mais d’autres attaques exploitent à leurs tours différentes failles, et ainsi de suite dans un cycle infernal.
Pour répondre à cette problématique et anticiper plutôt que réagir, l’équipe Spicy de l’IRISA dirigée par Stéphanie Delaune, développe des programmes de vérification de protocoles cryptographiques. « Notre objectif est de déceler des failles dans des protocoles existants à l’aide de méthodes formelles. Pour cela, nous modélisons mathématiquement chaque protocole et nous le vérifions à l’aide d’outils divers, plus ou moins automatiques, dont Squirrel », explique la chercheuse. Ce logiciel, en partie développé au sein de l’équipe Spicy, est un assistant de preuve qui accompagne le développeur pas à pas. Celui-ci renseigne son protocole, décrit sa méthode et les propriétés qu’il veut démontrer. Squirrel vérifie chaque étape de la preuve, détecte les erreurs de raisonnement, et, in fine, permet de proposer des recommandations afin d’améliorer la fiabilité du protocole face à des attaques.