La sécurité des logiciels critiques est aujourd’hui un enjeu majeur dans le monde informatique. De nouvelles attaques confirment chaque jour la nécessité d’investir plus dans les outils et les techniques qui permettent de réduire la vulnérabilité des systèmes informatique. Le plus souvent il suffit d’exploiter des failles dans l’un des modules du système d’exploitation pour compromettre la sécurité de toutes les applications qui s'exécutent au-dessus. Dans ce contexte, il existe plusieurs travaux autour de la vérification formelle des systèmes d’exploitation. Celle-ci se fonde sur des modèles mathématiques permettant de raisonner rigoureusement sur leurs comportements et prouver qu’ils sont corrects. Une grande majorité de ces travaux consiste à prouver des propriétés sur des systèmes de taille importante ce qui rend l’étape de la maîtrise de tous les détails de ce logiciel critique assez longue et donc la vérification devient plus compliquée à établir. Dans le domaine des systèmes embarqués, la construction de nouveaux noyaux est une activité récurrente. Ceci est motivé généralement par la taille réduite de ces systèmes. Mais leurs petites tailles rendent difficile la mise en œuvre de mesures de sécurité et de sûreté de fonctionnement. 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 micronoyau 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.
M. Gilles GRIMAUD - Université de Lille - Directeur de thèse M. David NOWAK - CNRS, Université de Lille - Encadrant M. Etienne RIVIERE - Ecole Polytechnique de Louvain - Rapporteur M. David PICHARDIE - Ecole normale supérieure de Rennes - Rapporteur Mme Sophie TISON - Université de Lille - Examinateur M. Timothy BOURKE - Ecole normale supérieure de Paris - Examinateur
Thèse de l'équipe 2XS soutenue le 20/12/2018
français
English