Phd Position F/m Verifying Memory Safety of Linux Kernel Drivers

Le descriptif de l’offre ci-dessous est en Anglais_

**Type de contrat**: CDD

**Niveau de diplôme exigé**: Bac + 5 ou équivalent

**Fonction**: Doctorant

**A propos du centre ou de la direction fonctionnelle**:
The Centre Inria de l’Université de Grenoble groups together almost 600 people in 26 research teams and 9 research support departments.

Staff is present on three campuses in Grenoble, in close collaboration with other research and higher education institutions (Université Grenoble Alpes, CNRS, CEA, INRAE,), but also with key economic players in the area.

The Centre Inria de l’Université Grenoble Alpes is active in the fields of high-performance computing, verification and embedded systems, modeling of the environment at multiple levels, and data science and artificial intelligence. The center is a top-level scientific institute with an extensive network of international collaborations in Europe and the rest of the world.

**Mission confiée**:
The Linux kernel is a large and complex codebase (millions of lines of code, mostly in C) which makes formal verification of its components a significant challenge. Device drivers, in particular, are often developed by third parties or maintained outside the mainline kernel, and are a frequent source of bugs, especially memory safety issues such as buffer overflows, dangling pointers, and use-after-free errors.

While verifying the entire kernel is currently out of reach, focusing on memory safety in drivers - which typically interact with the kernel through well-defined interfaces - offers a promising and tractable target for formal analysis.

**Objective**

The goal of this PhD is to formally verify the memory safety of Linux kernel drivers. The project will focus on driver interactions with the kernel, including the direct use of kernel APIs and shared memory structures.

**Principales activités**:
The work will involve:

- Selecting representative drivers and the kernel APIs they rely on.
- Defining memory safety properties relevant to these drivers (e.g., correct use of DMA buffers).
- Identifying common unsafe patterns or assumptions in the use of kernel APIs.
- Exploring tools (e.g., static analysis, symbolic execution, model checking, formal specification) to verify that drivers satisfy the defined safety properties.

Expected outcomes include a better understanding of the conditions under which drivers can be memory-safe, formal models or specifications of key driver-kernel interfaces, and verified case studies of existing drivers. This work could pave the way toward a more robust Linux kernel, offering stronger guarantees for one of its most vulnerable components.

**Compétences**:
Technical skills and level required : knowledge of Rust and C, prior experience with verification of low-level code

Languages : fluent Englis

**Avantages**:

- Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage (under conditions)

**Rémunération**:
2200 euros gross salary /month in 2025

2300 euros gross salary /month in 2026

**Informations générales**:

- **Thème/Domaine**: Systèmes distribués et intergiciels
Système & réseaux (BAP E)
- **Ville**: Saint Martin d'Héres
- **Centre Inria**: Centre Inria de l'Université Grenoble Alpes
- **Date de prise de fonction souhaitée**: 2025-10-01
- **Durée de contrat**: 3 ans
- **Date limite pour postuler**: 2025-09-25

**Consignes pour postuler**:
**Sécurité défense**:
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.

**Politique de recrutement**:
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.

**Contacts**:

- **Équipe Inria**: KRAKOS
- **Directeur de thèse**:
**A propos d'Inria**:
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à