24 septembre 2026 à 14h (INRIA Lille)
Les opérateurs télécoms prévoient un déploiement à grande échelle de fonctions réseau cloud-natives (CNF), gérées au moyen de Kubernetes, la plateforme d'orchestration de conteneurs de référence. Kubernetes repose sur deux mécanismes principaux : les manifestes, des fichiers de configuration déclaratifs qui décrivent l'état souhaité du système, et les opérateurs, des composants logiciels qui automatisent le cycle de vie d'applications complexes. Cependant, ces deux mécanismes sont sujets à des erreurs pouvant entraîner des interruptions de service, des failles de sécurité ou des fuites de ressources. Cette thèse propose KOMET, un cadre de vérification composé de deux sous composants complémentaires. Le premier, KOMETm, est dédié à la vérification des manifestes. Notre étude de 17~outils existants a montré qu'aucun ne réunit les cinq capacités que nous avons identifiées comme nécessaires à une vérification complète : la validation de schéma, la validation native, la validation des bonnes pratiques, l'évaluation de règles personnalisées et la détection d'incohérences. KOMETm comble ces lacunes. Sa contribution centrale est un mécanisme de détection d'incohérences qui traduit les règles CEL (Common Expression Language) en spécifications Alloy, permettant de vérifier automatiquement qu'un ensemble de règles de validation reste mutuellement satisfaisable. Le second composant, KOMETo, est dédié à la vérification des opérateurs Kubernetes. Il repose sur l'analyse statique du code source Go d'un opérateur pour en extraire automatiquement un modèle comportemental, puis vérifier des propriétés de correction contre ce modèle. Appliqué à 15~fonctions de réconciliation issues de 6~projets open source, KOMETo a mis en évidence des défauts dans chacun des projets étudiés, confirmant l'efficacité de l'approche.
M. Philippe MERLE Directeur de recherche Université de Lille Directeur de thèse, Mme Rabéa AMEUR-BOULIFA Maîtresse de conférences Télécom Paris Campus SophiaTech Rapporteure, Mme Hélène COULLON Maîtresse de conférences IMT Atlantique Examinatrice, M. Jean-Bernard STEFANI Directeur de recherche INRIA Grenoble Co-directeur de thèse, M. Roberto DI COSMO Professeur Université Paris Cité Rapporteur, M. Radu MATEESCU Directeur de recherche INRIA Grenoble Examinateur, M. Guillaume PIERRE Professeur Université de Rennes Examinateur, Mme Meryem OUZZIF Ingénieure de recherche Orange Co-encadrante de thèse, Mme Karine GUILLOUARD Orange Invitée.
français
English