Sujet de la thèse : Vérification de modules critiques d'hyperviseur avec la prise en compte des propriétés matérielles

Début de la thèse : 04/12/2025

Directeur de thèse : Frédéric LOULERGUE

Résumé :

Les hyperviseurs permettent à un système hôte de prendre en charge plusieurs systèmes invités (machines virtuelles, ou VM) en partageant virtuellement ses ressources, telles que la mémoire et la puissance de calcul. Déjà largement utilisés dans certains domaines (par exemple, les infrastructures cloud), les hyperviseurs sont aujourd'hui essentiels pour les systèmes embarqués critiques en raison du nombre croissant de fonctions et de caractéristiques nécessaires pour ces systèmes. On peut citer par exemple l'assistance à la conduite ou la gestion de capteurs, et d'autres doivent être intégrées, par exemple des solutions d'intelligence artificielle (IA) pour les systèmes critiques, ou encore des fonctionnalités de divertissement et de connectivité supplémentaires. Dans de nombreux contextes, l'ajout de matériel supplémentaire est impossible en raison des contraintes de taille, de poids et de coût. Pour permettre cette intégration, il est nécessaire de partager le même matériel entre plusieurs fonctions (ou systèmes), souvent avec différents niveaux de criticité. Ceci est possible grâce à la virtualisation, chaque système s'exécutant sur une VM distincte. Dans ce contexte, il est essentiel de garantir des propriétés de sécurité telles que l'isolation de la mémoire ou l'intégrité basée sur un élément sécurisé. De plus, ces garanties doivent prendre en compte les propriétés système et matérielles de bas niveau, ce qui représente souvent un défi pour les outils de vérification modernes. Objectifs. Des travaux récents de Thales ont démontré que la vérification formelle peut être appliquée à du code critique réel afin de garantir ses propriétés de sécurité. Thales a réalisé plusieurs certifications réussies EAL6-EAL7 de la machine virtuelle JavaCard utilisée dans ses produits. Ce projet de thèse est motivé par la nécessité d'étendre le périmètre des systèmes critiques pour la sécurité, formellement vérifiés et certifiés, aux systèmes utilisant des hyperviseurs. Innovation. L'innovation de ce projet doctoral réside dans une combinaison d'approches de vérification matérielle et logicielle tout en prenant en compte le code réel de l'hyperviseur (plutôt que son modèle de haut niveau), ce qui offre des garanties de sécurité fortes. Le travail s'appuiera sur les résultats innovants de la vérification en cours du cœur CVA6 chez Thales. Une autre ambition du projet est de cibler des hyperviseurs applicables à des systèmes embarqués réels.