Avec la croissance majeure de l’Internet des Objets et du Cloud Computing, la sécurité dans ces systèmes est devenue un problème majeur. Plusieurs attaques ont eu lieu dans les dernières années, mettant en avant la nécessité de garanties de sécurité fortes sur ces systèmes. La plupart du temps, une vulnérabilité dans le noyau ou un de ses modules est suffisante pour compromettre l’intégralité du système. Établir et prouver des propriétés de sécurité par le biais d’assistants de preuve semble être un grand pas en avant vers l’apport de garanties de sécurité. Cela repose sur l’utilisation de modèles mathématiques dans le but de raisonner sur leur comportement, et d’assurer que ce dernier reste correct. Cependant, en raison de la base de code importante des logiciels s’exécutant dans ces systèmes, plus particulièrement le noyau, cela n’est pas une tâche aisée. La compréhension du fonctionnement interne de ces noyaux, et l’écriture de la preuve associée à une quelconque propriété de sécurité, est de plus en plus difficile à mesure que le noyau grandit en taille. Dans cette thèse, je propose une nouvelle approche de conception de noyau, le proto-noyau. En réduisant les fonctionnalités offertes par le noyau jusqu’à leur plus minimal ensemble, ce modèle, en plus de réduire au maximum la surface d’attaque, réduit le coût de preuve au maximum. Il permet également à un vaste ensemble de systèmes d’être construits par-dessus, considérant que la minimalité des fonctionnalités comprises dans le noyau oblige les fonctionnalités restantes à être implémentées en espace utilisateur. Je propose également dans cette thèse une implémentation complète de ce noyau, sous la forme du proto-noyau Pip. En ne fournissant que les appels systèmes les plus minimaux et indispensables, l’adaptation du noyau à des usages concrets et la faisabilité de la preuve sont assurées. Afin de réduire le coût de transition modèle vers binaire, la majorité du noyau est écrite directement en Gallina, le langage de l’assistant de preuve Coq, et est automatiquement convertie en code C compilable pendant la phase de compilation. Pip ne repose alors que sur une fine couche d’abstraction matérielle écrite dans des langages de bas niveau, qui ne fournit que les primitives que le modèle requiert, telles que la configuration du matériel. De plus, étant donné que l’Internet des Objets et le Cloud Computing nécessitent aujourd’hui ces architectures, je propose plusieurs extensions au modèle de Pip afin de supporter le matériel multi-cœur. Soutenus par des implémentations, ces modèles permettent d’apporter le proto-noyau Pip dans les architectures multi-coeur, apportant ainsi des garanties de sécurité fortes dans ces environnement. Enfin, je valide mon approche et son implémentation par le biais d’évaluations de performances et d’une preuve de concept de portage de noyau Linux, démontrant ainsi la flexibilité du proto-noyau Pip dans des environnements réels.
M. Gaël THOMAS Telecom SudParis Rapporteur M. Sébastien MONNET Université Savoie Mont-Blanc Rapporteur M. Gilles GRIMAUD Université de Lille Directeur de thèse M. Julien CARTIGNY Université de Lille Co-directeur de thèse M. Noël DE PALMA Université Grenoble Alpes Examinateur Mme Fabienne BOYER Université Grenoble Alpes Examinateur
Thesis of the team 2XS defended on 19/06/2019
français
English