Thèse Optimisation de l'Inférence de Machine États Appliquée à la Sécurité en Utilisant des Technique d'Instrumentation Bas Niveau et le Checkpointing H/F

Institut Polytechnique de Paris Télécom SudParis

Établissement : Institut Polytechnique de Paris Télécom SudParis
École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris
Laboratoire de recherche : SAMOVAR - Services répartis, Architectures, Modélisation, Validation, Administration des Réseaux
Direction de la thèse : Olivier LEVILLAIN ORCID 0000000205585015
Début de la thèse : 2026-11-01
Date limite de candidature : 2026-04-10T23:59:59

De nombreux protocoles réseau, tels que TCP, TLS ou WPA, reposent sur une machine à états interne, qui peut soit être explicite (en utilisant des variables d'états) ou implicite (l'état effectif est alors encodé dans le graphe de l'appel de la pile). Parfois, cette machine à états dévie de la spécification implémentée et présente des buts intéressants, y compris des failles de sécurité telles que des contournements de l'authentification. Ces dernières années, des problèmes de machine à états ont été identifiés dans de nombreuses piles réseau très utilisées à l'aide de l'Active Automata Learning [2, 3, 4].

Une des limitations connue de cette approche, cependant, est que l'inférence peut prendre beaucoup de temps pour converger. En effet, le processus d'apprentissage consist à interagir avec la cible (appelée généralement SUL, pour System Under Learning) en envoyant des séquences de messages, y compris des séquences mal formées ou incohérentes, et en attendant la réponse du SUL pour caractériser son comportement. Comme la réponse peut contenir un nombre arbitraire de messages, il est nécessaire d'attendre en mettant en place un délai maximum (timeout) pour espérer obtenir une réponse complète.

Pendant la thèse d'Aina Rasoamanana [5], nous avons exploré des optimisations utilisant l'aspect déterministe de l'algorithme L* [1] que nous utilisons dans nos expériences. Malgré des résultats prometteurs (des gains de temps jusqu'à une division par 25 du temps d'inférence), nous avons identifié des goulets d'étranglement, qui sont également discutés dans la littérature [6] : l'initialisation du SUL, le temps perdu dans les changements de contexte liés et le temps passé à attendre l'expiration des timeouts.

Pour s'affranchir de ces limitations, la parallélisation et l'utilisation de mécanismes de checkpoint ont été étudiés [7], mais les résultats concernant le checkpointing étaient décevants. Nous croyons qu'une autre approche est possible, et qu'elle pourrait mener à des gains drastiques. Nous proposons de mettre en place des techniques d'instrumentation bas niveau en capturant les appels système. Une idée similaire a été proposée et implémentée pour améliorer les outils de fuzzing à états [6]; cette thèse a pour objectif de pousser cette idée plus loin dans un contexte plus complexe.

Pour capturer les appels système, nous proposons de pré-charger une bibliothèque partagée afin de surcharger l'interface fournie par la bibliothèque standard C, ce qui permet à notre outil d'inférence de surveiller précisément ce que le SUL est en train de faire. Cela nous permettra d'éviter de manière fiable l'attente inutile de messages. L'étape suivante sera d'embarquer l'ensemble de l'outil d'inférence comme une bibliothèque partagée, afin de se débarasser d'une bonne partie des changements de contexte. Enfin, cette approche serait idéale pour implémenter une nouvelle version du checkpointing, ce qui permettrait d'économiser complètement toute l'initialisation du SUL.

Un tel processus d'inférence amélioré serait assez rapide pour être inclus dans les pipelines d'intégration continue. Une autre application serait d'utiliser un vocabulaire plus large pour explorer des territoires inconnues et mener des analyses plus complexes. Cette thèse présente un grand nombre de défis intéressants à relever pour que les idées décrites ici fonctionnent correctement (par exemple la gestion de programmesmulti-processus et multi-threads, ou bien les usages d'appels système de manière exotique).

Most network stacks, e.g. TCP, TLS, or WPA, rely on an internal state machine, which can either be explicit (with the presence of state variables) or implicit (the actual state may be encoded in the call stack). Sometimes, this state machine deviates from the implemented specification and exhibits interesting bugs, including security flaws such as authentication bypass. In recent years, state machine issues have been identified in many high-profile network [2, 3, 4] using Active Automata Learning.

Active Automata Learning consists in interacting with a system we want to study (often called System Under Learning, or SUL) to infer the internal state machine from the observable behavior of the considered target. The domain takes its source from the seminal work of Angluin in 1987 [1] which describes the first inference algorithm, L*. Initially designed to work on Finite State Machines, it was later extended to cover Mealy Machines, a state machine model where edges are tagged both with the messages sent to the SUL and the answer received from the SUL.

One known limitation of this approach, however, is that the inference can be a very long process. Indeed, the learning process consists in sending sequences of messages to the SUL, including malformed or inconsistent ones, and wait for the SUL's answer to characterize its behavior. Since the response can consist of an arbitrary number of messages, we must rely on timeouts and hope we retrieved the complete answer.

During Aina Rasoamanana's thesis [5], we explored optimizations leveraging the deterministic aspect of the L* algorithm we rely on in our experiments. Despite promising results (up to 25-fold speedups), we identified several bottlenecks, also discussed in the literature [6]: the SUL initialization time, the time spent in context switches and the time wasted in the wait for timeouts.

This PhD proposal is part of a research activity on network protocol security, developed in the security team at Télécom SudParis since 2018: ANR GASP Project 2019-2024, IMT Carnot Télécom GINS Project, two PhD theses defended in 2023 [5]and 2025 [8], a postdoc, several publications [4, 9, 10].