Le co-design d’un noyau de système d’exploitation et de sa preuve formelle d’isolation

Dans cette thèse nous proposons un nouveau concept de noyau adapté à la preuve que nous avons appelé « proto-noyau ». Il s’agit d’un noyau de système d’exploitation minimal où la minimisation de sa taille est principalement motivée par la réduction du coût de la preuve mais aussi de la surface d’attaque. Ceci nous amène à définir une nouvelle stratégie de « co-design » du noyau et de sa preuve. Elle est fondée principalement sur les feedbacks entre les différentes phases de développement du noyau, allant de la définition des besoins jusqu’à la vérification formelle de ses propriétés. Ainsi, dans ce contexte nous avons conçu et implémenté le proto-noyau Pip. L’ensemble de ses appels système a été choisi minutieusement pendant la phase de conception pour assurer à la fois la faisabilité de la preuve et l’utilisabilité du système. Le code de Pip est écrit en Gallina (le langage de spécification de l’assistant de preuve Coq) puis traduit automatiquement vers le langage C. La propriété principale étudiée dans ces travaux est une propriété de sécurité, exprimée en termes d’isolation mémoire. Cette propriété a été largement étudiée dans la littérature de par son importance. Ainsi, nos travaux consistent plus particulièrement à orienter le développement des concepts de base de ce noyau minimaliste par la vérification formelle de cette propriété. La stratégie de vérification a été expérimentée, dans un premier temps, sur un modèle générique de micro-noyau que nous avons également écrit en Gallina. Par ce modèle simplifié de micro-noyau nous avons pu valider notre approche de vérification avant de l’appliquer sur l’implémentation concrète du proto-noyau Pip.