Sites Inria

Securité numérique

Jean-Michel Prima - 23/05/2017

Vérifier la sécurité des échanges de clés

sécurité

Membres du Pôle d'excellence cyber (PEC), Thales Communications & Security et le centre Inria Rennes - Bretagne Atlantique entament une collaboration pour réaliser la vérification formelle d'une implémentation d'IKEv2. Ce protocole d'échange de clés de chiffrement constitue l'un des mécanismes essentiels pour établir des communications sécurisées sur le réseau IP.  Explications. 

Whitfield Diffie et Martin Hellman ont récemment reçu le prix Turing, l'équivalent du Nobel pour l'informatique. En 1977, ces deux cryptographes américains imaginaient un moyen permettant à deux personnes d'échanger des nombres pour se mettre d'accord sur une clé qui servirait ensuite à chiffrer leurs messages. Particularité de cette technique : même en espionnant l'échange, il demeure impossible de recalculer cette clé. Aujourd'hui, le protocole Diffie-Hellman se trouve au cœur d'IKE (Internet-key exchange), le protocole chargé de négocier l'établissement de tunnels sécurisés sur le réseau IP.
« La collaboration que nous débutons avec Thales porte justement sur ce protocole », explique Axel Legay, le scientifique responsable de l'équipe Tamis au centre Inria de Rennes. L'industriel travaille actuellement sur une implémentation d'IKEv2 qu'il envisage d'intégrer - à terme -  dans certains de ses produits de sécurité réseau. Mais avant cela, il souhaite prendre toutes les assurances que l'implémentation d'une part respecte bien les spécifications du protocole et d'autre part ne soit pas elle-même vulnérable.

L'attaque par "l'homme du milieu"

Le risque ? « Ce que l'on appelle l'attaque par "l'homme du milieu". Un intrus intercepte la communication, se fait passer pour l'un des interlocuteurs et envoie sa propre clé dans le but d'accéder ensuite au chiffrement.  » Le protocole Diffie-Hellman peut succomber à ce type d'attaque, mais pas le protocole IKE, à condition de bien le mettre en œuvre.

Les travaux vont durer trois ans pendant lesquels l'entreprise va financer une thèse Cifre encadrée par l'équipe de recherche. « L'objectif de la thèse est de parvenir à une certification de cette implémentation. Ces recherches présentent donc une finalité très concrète en rapport direct avec les préoccupations de l'industriel. Par ailleurs, l'étudiant que nous allons encadrer, Tristan Ninet, a déjà travaillé pour Thales et participé à la conception de l'implémentation. Enfin, à Cholet, sur le site de l'entreprise, un ingénieur se consacre également à ce projet.  »
La collaboration porte sur deux points. « Le premier consiste à s'assurer que l'implémentation respecte bien toutes les spécificités du protocole. Le second concerne l'analyse de vulnérabilité dans l'implémentation elle-même. En effet, pour implémenter un protocole, il faut utiliser un langage de programmation. Or ce langage pourrait lui-même subir toute sorte d'attaques comme des dépassements de tampons ou encore des pointeurs morts. Il faut donc vérifier que le programme n'est pas vulnérable à ces attaques.  »

Détection automatique de vulnérabilité

Dans ce contexte, les scientifiques d'Inria apportent deux types de compétences.  « Tout d'abord des techniques de vérifications formelles comme le model checking et le test basé sur les modèles. Ces méthodes permettent de voir si l'implémentation satisfait aux spécifications du protocole. Ensuite, nous possédons une expérience en matière de fuzzing et d'analyse symbolique du code.  »
Pourquoi l'analyse symbolique ? « Quand on arrive dans le code lui-même, faire du model checking devient difficile. Concrètement, il faut aller regarder l'exécution du code. C'est un travail long et compliqué. Ceci d'autant plus qu'un attaquant peut introduire de l'obfuscation. D'où l'intérêt de l'analyse symbolique qui permet d'observer d'un coup plusieurs exécutions. Et là, nous apportons de l'expertise avec des outils de désobfuscation, de dévirtualisation du code.  »
Grâce à ces méthodes, l'équipe Tamis est en mesure de systématiser la détection automatique des vulnérabilités aux attaques déjà répertoriées. « Pour celles-ci, nous pourrons dire que nous avons une certitude de 100%. Mais il y a aussi les attaques que l'on ne connaît pas encore. Celles-là nous intéressent également beaucoup. Si nous venions à en découvrir, nous pourrions ensuite développer de nouvelles techniques pour assurer, là aussi, leur détection automatique, sachant que ces éventuelles vulnérabilités pourraient potentiellement exister dans d'autres implémentations.  »

Mots-clés : PEC TAMIS Chiffrement INRIA Rennes - Bretagne Atlantique Sécurité Thales

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !