Vérification de modules critiques d'hyperviseur avec la prise en compte des propriétés matérielles // Verification of critical modules of hypervisors taking into account hardware constraints

Hypervisors allow a host system to support multiple guest systems (virtual machines, or VMs) by virtually sharing its resources, such as memory and processing. Already intensively used in some domains (e.g. cloud infrastructures), hypervisors become highly relevant today for critical embedded systems due to an increasing number of necessary functions and features. Numerous functions have already been added to embedded systems, such as driver assistance or sensor management, and more functions need to be integrated today, for example, artificial intelligence (AI) solutions for mission-critical systems, or further entertainment and connectivity features. In many contexts, it is not possible to add more hardware because of size, weight and cost constraints. To enable this integration, it is necessary to share the same hardware between several functions (or systems), often with different levels of criticality. It can be achieved thanks to virtualization, when each system runs on a separate VM. In this context, security properties (such as memory isolation or integrity based on a secure element) are essential to guarantee. Moreover, these guarantees should take into account low-level system and hardware properties, which is often a challenge for modern verification tools.

Goals.

Recent work of Thales demonstrated that formal verification can be applied to critical real-life code in order to demonstrate its security properties. Thales realized several successful EAL6-EAL7 certifications of JavaCard Virtual Machine used in its products. This PhD project is motivated by the need to extend the perimeter of formally verified and certified security-critical systems to systems with hypervisors.

Innovation.

The innovation of this PhD project relies in a combination of hardware and software verification approaches while taking into account the real-life code of the hypervisor (rather than its high-level model) that provides strong security guarantees. The work will rely on innovative results of the ongoing verification of CVA6 at Thales. Another ambition of the project it to target hypervisors applicable to real-life embedded systems.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Hypervisors allow a host system to support multiple guest systems (virtual machines, or VMs) by virtually sharing its resources, such as memory and processing. Already intensively used in some domains (e.g. cloud infrastructures), hypervisors become highly relevant today for critical embedded systems due to an increasing number of necessary functions and features. Numerous functions have already been added to embedded systems, such as driver assistance or sensor management, and more functions need to be integrated today, for example, artificial intelligence (AI) solutions for mission-critical systems, or further entertainment and connectivity features. In many contexts, it is not possible to add more hardware because of size, weight and cost constraints. To enable this integration, it is necessary to share the same hardware between several functions (or systems), often with different levels of criticality. It can be achieved thanks to virtualization, when each system runs on a separate VM. In this context, security properties (such as memory isolation or integrity based on a secure element) are essential to guarantee. Moreover, these guarantees should take into account low-level system and hardware properties, which is often a challenge for modern verification tools.

Goals.

Recent work of Thales demonstrated that formal verification can be applied to critical real-life code in order to demonstrate its security properties. Thales realized several successful EAL6-EAL7 certifications of JavaCard Virtual Machine used in its products. This PhD project is motivated by the need to extend the perimeter of formally verified and certified security-critical systems to systems with hypervisors.

Innovation.

The innovation of this PhD project relies in a combination of hardware and software verification approaches while taking into account the real-life code of the hypervisor (rather than its high-level model) that provides strong security guarantees. The work will rely on innovative results of the ongoing verification of CVA6 at Thales. Another ambition of the project it to target hypervisors applicable to real-life embedded systems.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Cifre

CIFRE ANRT

Université d'Orléans

551 Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes - MIPTIS

Les candidats auront un BAC+5 en Informatique (un Master 2 ou un diplôme d'ingénieur) Des connaissances en génie logiciel ou vérification de programmes et un goût pour le raisonnement formel et la logique sont attendus.
Masters degree or equivalent. Software engineering and formal verification of programs and a taste for formal reasoning and logic.