The Cubicle Fuzzy Loop: A Testing Framework for Cubicle
Vendredi 8 décembre 2023 10h30
Université Paris-Saclay, bâtiment 650, salle 435 (salle des thèses)
Résumé. L’objectif de cette thèse est d’intégrer une technique de test dans le model checker Cubicle. Pour cela, nous avons étendu Cubicle avec une boucle de Fuzzing (appelée Cubicle Fuzzy Loop – CFL). Cette nouvelle fonctionnalité remplit deux fonctions principales. Tout d’abord, elle sert d’oracle pour l’algorithme de génération d’invariants de Cubicle. Ce dernier, basé sur une exploration en avant de l’ensemble des états atteignables, était fortement limité par ses heuristiques lorsqu’elles sont appliquées à des modèles fortement concurrents. CFL apporte une nouvelle manière plus efficace d’explorer ces modèles, en particulier il permet de visiter beaucoup plus d’états pertinents. Son deuxième objectif est de détecter rapidement et efficacement les problèmes et les vulnérabilités dans les modèles de toutes tailles, ainsi que de capturer les deadlocks. L’intégration de CFL nous a également permis d’augmenter l’expressivité du langage d’entrée de Cubicle, avec l’inclusion de nouvelles primitives pour manipuler des threads (verrous, sémaphores, etc.). Enfin, nous avons construit un cadre de test autour de Cubicle et de CFL avec un interpréteur interactif, utile pour le débogage, le prototypage et l’exécution pas à pas des modèles. Ce nouveau système a été appliqué avec succès sur une étude de cas d’un algorithme de consensus distribué pour blockchains.
Membres du jury:
- Mme Dominique QUADRI, Professeure des universités, Université Paris-Saclay - Examinateur
- Mme Régine LALEAU, Professeure des universités, Université Paris-Est Créteil - Rapporteur & Examinateur
- M. Stephan MERZ, Directeur de recherche, INRIA Nancy - Rapporteur & Examinateur
- M. Sylvain HALLÉ, Professeur des universités, Université du Québec à Chicoutimi - Examinateur
- M. Pascal POIZAT, Professeur des universités, Université Paris Nanterre - Examinateur
Encadrants:
- M. Sylvain CONCHON, Professeur des universités, Université Paris-Saclay - Directeur de thèse
- Mme. Fatiha ZAÏDI,Professeure des universités, Université Paris-Saclay - Co-encadrante de thèse
Résumé + Jury (EN):
Abstract
The goal of this thesis is to integrate a testing technique into the Cubicle model checker. To do this, we extended Cubicle with a Fuzzing loop (called the Cubicle Fuzzy Loop - CFL). This new feature serves two primary purposes. Firstly, it acts as an oracle for Cubicle’s in- variant generation algorithm. The existing algorithm, which is based on a forward exploration of reachable states, was significantly limited by its heuristics when applied to highly concurrent models. CFL introduces a more efficient way to explore these models, visiting a larger number of relevant states. Its second objective is to quickly and efficiently detect issues and vulnerabilities in models of all sizes, as well as detect deadlocks. The integration of CFL has also enabled us to enhance the expressiveness of Cubicle’s input language, including new primitives for manipulating threads (locks, semaphores, etc.). Lastly, we built a testing framework around Cubicle and CFL with an interactive interpreter, which is useful for debugging, prototyping, and step-by-step execution of models. This new system has been successfully applied in a case study of a distributed consensus algorithm for blockchains
Jury members:
- Dominique QUADRI, Professor, Université Paris-Saclay - Examiner
- Régine LALEAU, Professor, Université Paris-Est Créteil - Rapporteur & Examinateur
- Stephan MERZ, Senior Researcher, INRIA Nancy - Reviewer &
- Sylvain HALLÉ, Professor, Université du Québec à Chicoutimi - Examiner
- Pascal POIZAT, Professor, Université Paris Nanterre - Examiner
Supervisors:
- M. Sylvain CONCHON, Professor, Université Paris-Saclay - Thesis advisor
- Mme. Fatiha ZAÏDI, Professor, Université Paris-Saclay - Thesis co-supervisor