Prosecco : les protocoles cryptographiques sous bonne garde

Basée à Paris depuis sa création en 2012, l'équipe Prosecco développe une expertise en protocoles cryptographiques et en vérification de programmes pour contribuer à sécuriser les applications et les périphériques matériels. Sous la direction de Karthik Bhargavan elle compte aujourd'hui trois chercheurs permanents, trois chercheurs non permanents, trois postdoctorants, huit thésards et trois ingénieurs de recherche (femmes et hommes).

Étudier…

« Le premier volet de nos activités porte sur l'étude des propriétés de sécurité des protocoles notamment en matière de confidentialité, d'intégrité et d'authentification, explique Benjamin Beurdouche, doctorant au sein de l'équipe. Pour ce faire nous nous appuyons sur deux outils développés au sein de l’équipe : ProVerif et CryptoVerif. » Créés par Bruno Blanchet, directeur de recherche au sein de Prosecco, ils ont été mis à profit pour l'étude de nombreux protocoles, comme Signal qui est utilisé par les messageries instantanées comme WhatsApp ou Skype, WireGuard, un nouveau type de VPN qui pourrait prochainement être intégré au noyau de Linux ou encore le protocole ARINC qui sécurise les communications dans l’aviation civile..

…Implémenter…

En parallèle l'équipe travaille également à la création de langages de programmation et d'outils de vérification formelle. « Sur ce plan, notre outil phare est sans aucun doute le langage de programmation F*, développé dans le cadre du projet Everest, un partenariat entre Microsoft Research et Inria. F* est un langage fonctionnel conçu pour la vérification formelle et permet de générer du code C à haut niveau d'assurance tout en réduisant l'effort de preuve grâce à l’utilisation d’un prouveur automatique. » F* est lui-même au cœur du développement de projets très structurants pour l'équipe, comme la plate-forme de sécurité miTLS  ou HACL* , une bibliothèque cryptographique rapide et formellement vérifiée, sûre, correcte et sans canaux cachés dédiée à des applications comme les protocoles cryptographiques, la navigation web ou encore l'Internet des objets. Mise en production dans le navigateur Firefox de Mozilla , HACL* est aussi utilisée par Wireguard, la bibliothèque TLS de Facebook et la blockchain Tezos.

…Et créer les compilateurs de demain

Piloté par Cătălin Hriţcu, le dernier axe de recherche de Prosecco porte sur la compilation sécurisée. « Écrire des programmes ayant un haut niveau d’assurance est important mais insuffisant, souligne Benjamin Beurdouche. Bien que ces programmes soient soigneusement développés, ils s’exécutent dans un écosystème peuplé d’autres programmes avec lesquels ils interagissent. Ces composants logiciels extérieurs, sont parfois bogués, parfois malveillants, et ne sont pas contraints d’obéir aux règles imposées par le développeur ou la développeuse. Ils peuvent donc provoquer des failles de sécurités par composition. La "compilation sécurisée" a pour objectif de construire une nouvelle génération de compilateurs qui garantissent la préservation de la sécurité des programmes développés dans des langages de haut niveau, même en présence d’adversaires. »

TLS 1.3, MLS , des projets de grande ampleur

« Plusieurs projets phares de l'équipe se situent à l'interface de nos axes de recherche, ajoute Benjamin Beurdouche. C'est le cas notamment des travaux que nous avons menés de 2014 à 2018 autour du protocole de communication sécurisé du Web : TLS 1.3 qui a été approuvé en août dernier par l'IETF (Internet Engineering Task Force), l'un des organismes d'élaboration des standards Internet. Nous avons à la fois étudié les propriétés de sécurité de ce protocole utilisé chaque jour par des milliards de personnes mais aussi contribué activement à son design. » Depuis peu, un chantier du même type est en train de se mettre en place pour MLS (Messaging Layer Security), un protocole de communication sécurisée destiné aux messageries de groupe, également porté par l'IETF , avec le soutien de géants du Web comme Google, Facebook, Microsoft, Mozilla…

 

« L'enjeu est énorme car la messagerie de groupe fait figure de "parent pauvre" en termes de sécurisation. Pour l'heure le protocole de référence est Signal, mais son fonctionnement, établissant de nombreuses connections, limite la taille des groupes de discussion. Avec MLS l’idée est de fournir une solution fiable pour des groupes de plusieurs dizaines de milliers de personnes, ce qui ouvrirait des perspectives inédites. Et cette fois-ci Prosecco ne sera pas seulement contributeur mais bel et bien l'un des auteurs du futur protocole qui devrait voir le jour d’ici deux ans ! », annonce Benjamin Beurdouche en conclusion.