Microsoft et Inria contribuent à renforcer TLS

Microsoft et Inria ont profité de l’Open Source Summit parisien pour présenter deux ensembles de codes libres associés au projet miTLS. Ce projet consiste en une implémentation de référence vérifiée du protocole TLS. Il est porté par les équipes du centre de recherche conjoint de l’institut et de l’éditeur.

Le code de la version stable de cette implémentation, en F#, est disponible sur GitHub, aux côtés de ses spécifications en F7. La version de développement de miTLS est rédigée en F*, un langage fonctionnel conçu pour la vérification de programmes, développé justement au sein d’Inria, en partenariat avec Microsoft, ENS Paris, et l’Université du Maryland.

Ce sont ces chercheurs du centre de recherche conjoint d’Inria et de Microsoft qui ont précédemment dévoilé les vulnérabilités Freak et Logjam, celle-ci affectant l’échange de clés. Dans un billet de blog, l’un des chercheurs explique d’ailleurs que ces vulnérabilités ont en fait été découvertes par hasard, alors que l’équipe travaillait déjà à une implémentation sûre du protocole TLS.

Le projet miTLS apparaît ainsi comme une initiative de long terme visant à « créer un système dont la sécurité puisse être prouvée mathématiquement ». Les chercheurs associés au projet ont par ailleurs « travaillé étroitement avec les experts de sécurité de toute l’industrie qui travaillent à la prochaine génération du protocole TLS », attendue pour 2016.

Pour Karthikeyan Bhargavan, l’un des chercheurs impliqués dans le projet, l’un des points les plus intéressants est justement là : « nous influençons la prochaine génération ». De quoi aider cette dernière à « réduire l’écart » entre les modèles de sécurité théoriques et leur mise en œuvre, comme le souligne pour sa part Cédric Fournet.