English version: see here.
Je vais soutenir ma thèse, intitulée "Vérification formelle et évaluation d'allocateurs mémoires", le vendredi 5 décembre 2025 à 14h ! La soutenance aura lieu au centre de recherche Inria Paris au 48 rue Barrault, 75013 Paris, dans l'amphithéâtre Jacques-Louis Lions.
La version la plus à jour du manuscrit est disponible ici (en anglais).
La composition du jury est la suivante.
Le logiciel est devenu omniprésent dans la vie quotidienne. La plupart des logiciels couramment utilisés, tels que les navigateurs Web, les applications de messagerie instantanée, les suites bureautiques ainsi que les outils de visioconférence, s'appuient sur la mémoire pour traiter des contenus variés, tels que des images, de la musique, des vidéos ou encore des documents au format PDF. L'allocateur mémoire est le composant logiciel qui est chargé de fournir à ces logiciels de la mémoire lors de leur exécution. Malheureusement, les applications utilisateur ne manipulent pas toujours la mémoire correctement. Dans les faits, de tels logiciels communément utilisés sont affectés par une classe de problèmes de sécurité étroitement liés à la gestion de la mémoire, appelés problèmes de sûreté mémoire. Pour limiter les impacts de ces problèmes, il est possible d'utiliser des allocateurs mémoire dits renforcés, chargés à la fois de subvenir aux besoins en mémoire des applications utilisateurs ainsi que de pallier les problèmes de sûreté mémoire de celles-ci. Compte tenu de leur rôle crucial, il est souhaitable de s'assurer que ces briques logicielles délicates sont fiables et correctes, ce qui motive l'emploi de méthodes formelles qui permettent de placer davantage de confiance dans les logiciels auxquels elles sont appliquées.
Dans le cadre de cette thèse, nous présentons une méthodologie pour prouver la correction fonctionnelle d'allocateurs mémoire renforcés, que nous utilisons pour le développement de StarMalloc, un allocateur mémoire vérifié, efficace, renforcé et concurrent. En utilisant le cadriciel de vérification Steel s'appuyant sur la logique de séparation, nous montrons comment spécifier et vérifier un ensemble varié de structures bas niveau et de mécanismes de sécurité complexes. Pour ce faire, nous nous appuyons sur la combinaison de types dépendants, de l'usage d'un solveur SMT et d'abstractions modulaires, qui permet un processus de vérification efficace et itératif.
Nous produisons un artefact vérifié, en C, qui implémente l'entièreté de l'interface de programmation d'un allocateur et peut ainsi être utilisé comme tel pour des projets réalistes tels que le navigateur Firefox. Ensuite, nous évaluons StarMalloc et démontrons que ses performances sont compétitives en le comparant à d'autres allocateurs sur un ensemble de tests de performance réalistes. Enfin, dans le but de mieux comprendre le comportement des allocateurs mémoire, nous avons développé un prototype permettant de tracer les opérations de gestion de la mémoire sur le tas, l'ensemble s'appuyant sur des fonctions matérielles.