Cette thèse a pour objet la conception d'un hyperviseur logiciel sécurisé, à vocation de certification. Les plus hauts niveaux de certification requièrent l'usage de méthodes formelles, permettant de démontrer la validité d'un produit par rapport à une spécification à l'aide de la logique mathématique. Le matériel prouvé n'existant pas, les mécanismes d'hypervision sont implémentés en logiciel. Cela contribue à réduire la base de confiance, et donc la quantité de modélisation et de preuve à produire. En outre, cela rend possible la virtualisation de systèmes sur des plateformes qui ne sont pas dotées d'instructions de virtualisation. Les principaux challenges sont l'analyse du jeu d'instruction qui, malgré l'existence de documentation, comporte des ambiguïtés, des particularités dépendantes de l'implémentation et des comportements non définis. Puis, l'identification des intensions d'un système invité étant donné un flot d'instructions discret afin de rester en interposition avec le matériel sous-jacent. Pour ce faire, le code machine de l'invité est analysé et les instructions menaçant l'intégrité ou la confidentialité du système sont remplacées par des trapes logicielles, provoquant une analyse du contexte afin d'autoriser ou non leur exécution. Reposant sur l'existence d'un CPU et d'une MMU prouvés, seul du code privilégié est susceptible d'outrepasser les droits d'accès configurés par l'hyperviseur. Il n'est donc pas nécessaire d'hyperviser le code non privilégié. Les micro-noyau, généralement choisis pour leur légèreté, ont donc un second avantage : ils réduisent au minimum le surcoût de l’hypervision.
- Directeur(s) de thèse :Gilles Grimaud, Michaël Hauspie - Rapporteurs : Issa Traoré Univ. Victoria (Canada) – Gaël Thomas (Télécom Sud Paris) - Examinateur : Isabelle Ryl (Inria Paris)
Thèse de l'équipe 2XS soutenue le 08/12/2016
français
English