Etude, spécification, vérification formelle de mécanismes de virtualisation sécurisés pour architecture many-cores

Cette thèse présente une solution de co-hébergement sécurisée de plusieurs piles logicielles autonomes sur une même puce pouvant comprendre jusqu à plusieurs centaines de coeurs. Dans le monde des puces généralistes, le nombre de coeurs ne cesse d augmenter rendant les machines de plus en plus puissantes. Pourtant, du point de vue de la sécurité, les machines n ont jamais été aussi vulnérables aux attaques alors qu elles traitent des informations d une sensibilité croissante. Les techniques actuelles d isolation, qu elles soient au niveau processus ou au niveau noyau, ne suffisent pas pour assurer la confidentialité, l intégrité et la disponibilité des entités logicielles en exécution. C est pourquoi nous proposons une virtualisation adaptée aux puces many-cores, permettant à des piles logicielles distinctes et potentiellement dangereuses de s exécuter dans un environnement de confiance dont la couche logicielle a été formellement vérifiée conforme à une spécification.This thesis presents a co-hosting approach of multiple software stacks within a same multiprocessor system-on-chip. In the eld of general purpose multiprocessors, the cores number is continuously increasing and so is the computation capability. But, from the trust side, this growing computer complexity deepens trust issues. This lack of trustworthiness is exacerbated by the increasing information s value processed by computer systems. Usual isolation techniques, at both user s or kernel s levels, do not offer enough protection for the con dentiality, integrity and availability of the running software stacks. In this thesis, we present a trusted many-cores virtualization approach which aims to execute software stacks in trusted virtual machines. Our goal is to provide enough isolation so a malicious virtual machine user will not be able to compromise another virtual machine. We have built hardware protection mechanisms which are under the control of a software formally veri ed hypervisor.PARIS-BIUSJ-Mathématiques rech (751052111) / SudocSudocFranceF