Thesis of Boubacar Diarra

KOMET: Un Framework de Vérification pour des Déploiements Fiables basés sur Kubernetes

Telecoms operators are planning a large-scale deployment of Cloud-Native Network Functions (CNFs), managed through Kubernetes, the de facto container orchestration platform. Kubernetes relies on two primary mechanisms: manifests, declarative configuration files that describe the desired state of a system, and operators, software components that automate the lifecycle management of complex applications. However, both mechanisms are prone to errors that can lead to service disruptions, security vulnerabilities, or resource leaks. This dissertation proposes KOMET, a verification framework composed of two complementary sub-components. The first, KOMETm, is dedicated to manifest verification. Based on a survey of 17~existing tools, we found that none simultaneously supports the five validation capabilities we identified as necessary for comprehensive verification: schema validation, native validation, best-practice validation, user-defined rule evaluation, and inconsistency detection. KOMETm fills these gaps. Its central contribution is an inconsistency detection mechanism that translates CEL (Common Expression Language) rules into Alloy specifications, enabling the tool to automatically verify that a set of validation rules remains mutually satisfiable. The second component, KOMETo, is dedicated to Kubernetes operator verification. It relies on static analysis of the Go source code of an operator to automatically extract a behavioral model and then verify correctness properties against that model. Applied to 15 reconciliation functions drawn from 6~open-source projects, KOMETo uncovered defects in every project examined, confirming the effectiveness of the approach.

Jury

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.

Thesis of the team Spirals defended on 24/09/2026