AVIS DE SOUTENANCE de Monsieur Aina Toky RASOAMANANA

L’Ecole doctorale : Ecole Doctorale de l’Institut Polytechnique de Paris
et le Laboratoire de recherche SAMOVAR

présentent

l’AVIS DE SOUTENANCE de Monsieur Aina Toky RASOAMANANA

AutorisĂ© Ă  prĂ©senter ses travaux en vue de l’obtention du Doctorat de l’Institut Polytechnique de Paris, prĂ©parĂ© Ă  TĂ©lĂ©com SudParis en :

Informatique

« Dérivation et analyse des implémentations des protocoles cryptographiques »

le JEUDI 8 JUIN 2023 Ă  14h00

Salle 3A213
19 Pl. Marguerite Perey, 91120 Palaiseau

Membres du jury :

M. HervĂ© DEBAR, Professeur, TĂ©lĂ©com SudParis, FRANCE – Directeur de thèse
M. Karthikeyan BHARGAVAN, Directeur de recherche, INRIA Paris, FRANCE – Rapporteur
Mme Barbara FILA, MaĂ®tresse de confĂ©rences, INSA Rennes, FRANCE – Rapporteure
Mme Marine MINIER, Professeure des universitĂ©s, UniversitĂ© de Lorraine, FRANCE – Examinatrice
M. AurĂ©lien FRANCILLON, Professeur, EURECOM, FRANCE – Examinateur
M. Fontaine ARNAUD, Responsable d’un laboratoire de l’ANSSI, Agence Nationale de la SĂ©curitĂ© des Systèmes d’Information (ANSSI), FRANCE – Examinateur
M. Olivier LEVILLAIN, MaĂ®tre de confĂ©rences, TĂ©lĂ©com SudParis, FRANCE – Co-encadrant de thèse

Résumé :

TLS et SSH sont deux protocoles de sĂ©curitĂ© très rĂ©pandu et Ă©tudiĂ©s par la communautĂ© de la recherche. Dans cette thèse, nous nous concentrons sur une classe spĂ©cifique de vulnĂ©rabilitĂ©s affectant les implĂ©mentations TLS et SSH, tels que les problèmes de machine Ă  Ă©tats. Ces vulnĂ©rabilitĂ©s sont dues par des diffĂ©rences d’interprĂ©tation de la norme et correspondent Ă  des Ă©carts par rapport aux spĂ©cifications, par exemple l’acceptation de messages non valides ou l’acceptation de messages valides hors sĂ©quence. Nous dĂ©veloppons une mĂ©thodologie gĂ©nĂ©ralisĂ©e et systĂ©matique pour dĂ©duire les machines d’Ă©tat des protocoles tels que TLS et SSH Ă  partir de stimuli et d’observations, et pour Ă©tudier leur Ă©volution au fil des rĂ©visions. Nous utilisons l’algorithme L* pour calculer les machines d’Ă©tat correspondant Ă  diffĂ©rents scĂ©narios d’exĂ©cution. Nous reproduisons plusieurs vulnĂ©rabilitĂ©s connues (dĂ©ni de service, contournement d’authentification) et en dĂ©couvrons de nouvelles. Nous montrons Ă©galement que l’infĂ©rence des machines Ă  Ă©tats est suffisamment efficace et pratique dans de nombreux cas pour ĂŞtre intĂ©grĂ©e dans un pipeline d’intĂ©gration continue, afin d’aider Ă  trouver de nouvelles vulnĂ©rabilitĂ©s ou dĂ©viations introduites au cours du dĂ©veloppement. Grâce Ă  notre approche systĂ©matique en boĂ®te noire, nous Ă©tudions plus de 600 versions diffĂ©rentes d’implĂ©mentations de serveurs et de clients dans divers scĂ©narios (versions de protocoles, options). En utilisant les machines d’Ă©tat rĂ©sultantes, nous proposons un algorithme robuste pour identifier les piles TLS et SSH. Il s’agit de la première application de cette approche sur un pĂ©rimètre aussi large, en termes de nombre de piles TLS et SSH, de rĂ©visions ou de scĂ©narios Ă©tudiĂ©s.


Abstract : « Derivation and Analysis of Cryptographic Protocol Implementation »

TLS and SSH are two well-known and thoroughly studied security protocols. In this thesis, we focus on a specific class of vulnerabilities affecting both protocols implementations, state machine errors. These vulnerabilities are caused by differences in interpreting the standard and correspond to deviations from the specifications, e.g. accepting invalid messages, or accepting valid messages out of sequence. We develop a generalized and systematic methodology to infer the protocol state machines such as the major TLS and SSH stacks from stimuli and observations, and to study their evolution across revisions. We use the L* algorithm to compute state machines corresponding to different execution scenarios. We reproduce several known vulnerabilities (denial of service, authentication bypasses), and uncover new ones. We also show that state machine inference is efficient and practical enough in many cases for integration within a continuous integration pipeline, to help find new vulnerabilities or deviations introduced during development. With our systematic black-box approach, we study over 600 different versions of server and client implementations in various scenarios (protocol versions, options). Using the resulting state machines, we propose a robust algorithm to fingerprint TLS and SSH stacks. To the best of our knowledge, this is the first application of this approach on such a broad perimeter, in terms of number of TLS and SSH stacks, revisions, or execution scenarios studied.