Amélioration de l'implémentation des protocoles cryptographiques grâce à l'inférence grammaticale

Les protocoles réseaux cryptographiques, tels que SSH et OPC UA, sont essentiels dans la sécurisation des communications. Cependant, leurs spécifications sont souvent longues, ambiguës et incomplètes, entraînant des erreurs d'implémentation et des vulnérabilités exploitables. Sans accès au code source, la vérification de la conformité d'une implémentation à sa spécification devient particulièrement complexe et se limite à l'analyse des échanges avec l'implémentation. L'apprentissage actif d'automates (Active Automata Learning, AAL) permet de construire un automate pour la vérification formelle, via des interrogations dynamiques de l'implémentation. Toutefois, le coût élevé de cette méthode limite son adoption pratique. Cette thèse propose plusieurs contributions visant à améliorer l'efficacité et l'applicabilité de l'analyse de protocoles basée sur les automates. Tout d'abord, elle introduit un cadre unifié pour l'apprentissage actif adaptatif, permettant d'exploiter des spécifications partielles ou des modèles issus de versions antérieures afin de guider le processus d'apprentissage. Ce cadre généralise les stratégies adaptatives existantes et facilite l'intégration de nouvelles, aboutissant à un nouvel algorithme adaptatif, ALλ, qui réalise à la fois des gains de performance et permet d'étudier les limites de l'apprentissage actif adaptatif. Ensuite, elle s'attaque aux limites de la phase de vérification en présentant le Mealy Verifier, un outil spécialisé capable de fournir rapidement des ensembles exhaustifs de contre-exemples pour des propriétés spécifiques aux protocoles. Cet outil réduit le besoin d'itération d'extraction de modèle et de vérification. La méthode proposée est validée au travers d'études de cas sur OPC UA et SSH, permettant la découverte de vulnérabilités inédites. Enfin, dans un projet de recherche distinct mené durant la thèse, un protocole de stockage multi-cloud sécurisé est conçu et implémenté sous forme de preuve de concept, offrant des garanties renforcées en matière de confidentialité, d'intégrité et de récupérabilité des fichiers. Dans l'ensemble, ces travaux contribuent à rendre les méthodes formelles plus pratiques et plus évolutives pour la vérification des protocoles dans des environnements réels.