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.