Skip to content. | Skip to navigation

Emergences

Lettre d'information n° 45

Image emergences pour impression
Personal tools
You are here: Home 2017 Lettre d'information n° 45 Vérifier la sécurité des échanges de clés
Document Actions

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

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.

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 (1) 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 (2) 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 toutes sortes 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 (3) 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. »

-------
Notes :

(1) Threat Analysis and Mitigation for Information Security. Tamis est une équipe Inria commune à l'Irisa.

(2)  Le dispositif CIFRE permet à l'entreprise de bénéficier d'une aide financière pour recruter un jeune doctorant dont les travaux de recherche, encadrés par un laboratoire public, conduiront à la soutenance d'une thèse.

(3) Test à données aléatoires pour mettre le logiciel à rude épreuve.