Agenda

Soutenance de doctorat de Karolina Gorna : Détection automatique de vulnérabilités dans Go

Jeudi 8 octobre 2026 à 14h00 (heure de Paris) à Télécom Paris

Télécom Paris, 19 place Marguerite Perey F-91120 Palaiseau [y aller], amphi 2

Titre intégral : Détection automatique de vulnérabilités dans Go : exécution concolique de binaires de programmes concurrents

Titre original : Automated Vulnerability Detection in Go: Concolic Execution for Multi-Threaded Binaries

Jury

  • David MONNIAUX, Directeur de recherche, CNRS et Université Grenoble Alpes, VERIMAG (Rapporteur)
  • Jean-Yves MARION, Professeur, Université de Lorraine / CNRS / École Nationale Supérieure des Mines de Nancy (Rapporteur)
  • Lesly-Ann DANIEL, Assistant professor, EURECOM (Examinatrice)
  • Pierre WILKE, Associate Professor, CentraleSupélec (Examinateur)
  • Rida KHATOUN, Professeur, Télécom Paris, Institut Polytechnique de Paris (Directeur de thèse)
  • Yannick SEURIN, Docteur, Ledger Donjon (Co-encadrant de thèse)
  • Nicolas IOOSS, Ingénieur, Ledger Donjon (Invité)
  • Robin DAVID, Docteur, Epsilon (Invité)

Résumé

Go est devenu un langage dominant pour les infrastructures cloud et blockchain, mais la plupart des outils d’analyse de binaires visent C, C++ ou Java et ne gèrent pas les exécutables volumineux et liés statiquement, les conventions d’appel non standard et le runtime M:N embarqué que produit la chaîne d’outils Go. Cette thèse développe Zorya, un moteur d’exécution concolique au niveau binaire pour le code Go compilé, fondé sur la représentation intermédiaire P-Code de Ghidra et le solveur SMT Z3.

En savoir plus
Trois contributions sont présentées. D’abord, LogicBombs-Go, un corpus de référence de 25 programmes Go annotés par leur condition de déclenchement, compilés avec les chaînes TinyGo et gc. Ensuite, un moteur mono-thread qui interprète le P-Code sur un modèle fidèle du processeur et de la mémoire x86-64, détecte les vulnérabilités au niveau des micro-opérations et explore les branches non prises au moyen d’une cascade de filtres guidée par les sites de panique. Enfin, une extension aux binaires compilés avec gc, dont le runtime est multi-thread, par la restauration de l’état de tous les threads, la neutralisation contrôlée de la préemption et l’exécution concolique par superposition (copy-on-write) qui rejoue les branches non prises et détecte des vulnérabilités silencieuses telles que les débordements d’entiers. L’évaluation de cette extension porte sur des classes de vulnérabilités séquentielles dans des artefacts gc multi-threads, sous une politique d’ordonnancement main-only ; l’exploration systématique des entrelacements de goroutines est préparée par Volos mais reste une perspective. Sur des vulnérabilités réelles issues de Kubernetes, Go-Ethereum et d’autres projets en production, Zorya détecte des bogues que les analyseurs statiques et les exécuteurs symboliques de binaires manquent, et une campagne de divulgation a révélé vingt-deux résultats supplémentaires. Zorya fonctionne sur des artefacts compilés sans instrumentation du code source ni harnais de fuzzing ; le mode fonction actuellement évalué s’appuie toutefois sur les informations DWARF et sur des symboles non supprimés pour récupérer les arguments. Il est publié en logiciel libre.