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. / In this thesis we propose a new kernel concept adapted to verification that we have called protokernel. It is a minimal operating system kernel where the minimization of its size is motivated by the reduction of the cost of proof and of the attack surface. This leads us to define a new strategy of codesign of the kernel and its proof. It is based mainly on the feedbacks between the various steps of development of the kernel, ranging from the definition of its specification to the formal verification of its properties. Thus, in this context we have designed and implemented the Pip protokernel. All of its system calls were carefully identified during the design step to ensure both the feasibility of proof and the usability of the system. The code of Pip is written in Gallina (the specification language of the Coq proof assistant) and then automatically translated into C code. The main property studied in this work is a security property, expressed in terms of memory isolation. This property has been largely discussed in the literature due to its importance. Thus, our work consists more particularly in guiding the developer to define the fundamental concepts of this minimalistic kernel through the formal verification of its isolation property. The verification strategy was first experimented with a generic microkernel model that we also wrote in Gallina. With this simplified microkernel model we were able to validate our verification approach before applying it to the concrete implementation of the Pip protokernel.

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èlevers-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. / Due to the major growth of the Internet of Things and Cloud Computing worlds, security in those systems has become a major issue. Many exploits and attacks happened in the last few years, highlighting the need of strong security guarantees on those systems. Most of the times, a vulnerability in the kernel or one of its modules is enough to compromise the whole system. Etablishing and proving security properties through proof assistants seems to be a huge step towards bringing security guarantees. This relies on using mathematical models in order to reason on their behaviour, and prove the latter remains correct. Still, due to the huge and complex code base of the software running on those systems, especially the kernel, this is a tedious task. Understanding the internals of those kernels, and writing an associated proof on some security property, is more and more difficult as the kernel grows in size. In this thesis, I propose a new approach of kernel design, the proto-kernel. By reducing the features provided by the kernel to their most minimal subset, this model, in addition to lowering the attack surface, reduces the cost of the proof effort. It also allows a wide range of systems to be built on top of it, as the minimality of the features embedded into the kernel causes the remaining features to be built at the userland level. I also provide in this thesis a concrete implementation of this model, the Pip proto-kernel. By providing only the most minimal and mandatory system calls, both the usability of the kernel and the feasibility of the proof are ensured. In order to reduce the model-to-binary transition effort, most of the kernel is written directly in Gallina, the language of the Coq Proof Assistant, and is automatically converted to compilable C code during compilation phase. Pip only relies on a thin hardware abstraction layer written in low-level languages, which provides the operations the model requires, such as modifying the hardware configuration. Moreover, as Internet of Things and Cloud Computing use cases would require, I propose some extensions of Pip’s model, in order to support multicore hardware. Backed up by real implementations, those models bring the Pip proto-kernel to multicore architectures, bringing strong security guarantees in those modern environments. Finally, I validate my approach and its implementation through benchmarks and a Linux kernel port proof-of-concept, displaying the flexibility of the Pip proto-kernel in real world environments.