Thèse de Florian Vanhems

Conception, implémentation et preuve d’un service de transfert de flôt d’exécution au sein d’un noyau de système d’exploitation

This file should contain the abstract. Le travail présenté dans ce document de thèse est lié à la vérification formelle de propriétés sur des systèmes d'exploitation. Les premiers travaux piliers de ce domaine sont ceux du projet SeL4 ; qui démontrent que la vérification de propriétés formelles sur un micro noyau est tout à fait réalisable, bien que très coûteux. Pour réduire le coût de la preuve, le projet CertikOS a produit une preuve plus étagée et plus modulaire, en tirant à l'extrême la méthode de preuve par raffinement. L'équipe du noyau Pip a pris le contrepied des travaux de CertikOS et SeL4, en utilisant une méthodologie reposant sur un shallow embedding et en prouvant directement les propriétés plutôt qu'en utilisant la méthode par raffinement. Les travaux présentés dans cette thèse sont plus spécifiquement liés au noyau Pip. Les travaux précédents sur le noyau Pip ont portés sur une preuve de préservation de l'isolation des services fournis par Pip manipulant la mémoire. Cependant, un aspect critique du noyau devait encore être conçu : le transfert de flôt d'exécution d'une partition de mémoire à une autre. La première contribution de cette thèse présente un nouveau service de Pip conçu pour supporter tous les transferts de flôts d'exécution possible au sein d'un système -- les interruptions, les fautes, et les appels explicites. Ce service est minimaliste -- les différentes portions de code sont réutilisées pour réduire davantage l'effort de preuve. Une implémentation est proposée pour le noyau Pip. Nous défendons l'idée que le concept derrière ce service est assez général pour être implémenté dans n'importe quel noyau. La seconde contribution de cette thèse est la première implémentation au monde d'un ordonnanceur Earliest Deadline First pour jobs arbitraires muni d'une preuve formelle. La preuve garantit que la fonction d'élection respecte la politique EDF, qui garantit l'optimalité du planning sur les machines mono-processeur. La preuve a été conduite en suivant la méthodologie habituelle de Pip, utilisant un shallow embedding et une monade d'état. Elle a cependant été réalisée par raffinement. De plus, l'ordonnanceur présenté utilise le service décrit précédemment afin de transférer le flot d'exécution, ce qui montre en prime sa polyvalence et son utilisabilité. La dernière contribution présentée dans cette thèse est une preuve de concept d'une monade d'état générique appliquée au noyau Pip. Cette monade générique permet de créer des modèles indépendants de la machine, permettant à priori de prouver plus simplement des propriétés spécifiques sur ces modèles. Cette contribution ouvre une nouvelle perspective de recherche sur la méthodologie de preuve, car elle devrait permettre de réduire considérablement le coût d'ajout de nouvelles propriétés au noyau. Néanmoins, utiliser cette technique ne permet à priori pas d'alléger la preuve de composition des propriétés des différents modèles.

Jury

M. Gilles GRIMAUD Université de Lille Directeur de thèse Mme Julia LAWALL INRIA Paris Rapporteure M. Emmanuel BACCELLI Freie Universität Berlin Rapporteur M. David NOWAK Centre de Recherche en Informatique, Signal et Automatique de Lille Examinateur M. Lionel RIEG Université Grenoble Alpes Examinateur M. Sylvain SALVATI Université de Lille Examinateur

Thèse de l'équipe 2XS soutenue le 02/03/2023