Supervision : Alain GREINER

Co-supervision : WAJSBÜRT Franck

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 cœurs. Dans le monde des puces généralistes, le nombre de cœurs 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.

2012-2013 Publications

• 2013
  • G. Plouviez, E. Encrenaz, F. Wajsbürt : “A formally verified hypervisor with hardware support for a many-core chip”, The 1^st Workshop on Runtime and Operating Systems for the Many-core Era, ROME 2013, vol. 8374, Lecture Notes in Computer Science, Aachen, Germany, pp. 801-811, (Springer) (2013)
• 2012
  • G. Plouviez : “Etude, spécification, vérification formelle de mécanismes de virtualisation sécurisés pour architecture many-cores”, thesis, phd defence 01/19/2012, supervision Greiner, Alain, co-supervision : Wajsbürt, Franck (2012)