Votre rôle est d’effectuer un travail de thèse sur : “ l’extension du noyau Linux par des programmes utilisateurs sûrs “.
 Contexte global et problématique du sujet

Le noyau du système d’exploitation représente un point d’observation privilégié qui permet de collecter à la fois des données de niveau infrastructure et des données d’observation applicatives. Le noyau offre également un point d’observation pour les deux activités réseau et système que peut avoir toute application s’exécutant au sein d’une plateforme télécom. Le langage eBPF (extended Berkeley Packet Filter) a révolutionné les pratiques d’observation en permettant l’exécution de programmes d’observation écrits en espace utilisateur au niveau du noyau Linux. La technologie eBPF comprend plusieurs éléments comme les helpers, les maps, ainsi que le vérifier. L’ensemble de ces composants permet aux programmes eBPF de bénéficier d’un large accès aux fonctions du noyau tout en offrant des garanties de sûreté.
Plusieurs services de gestion réseau et système ont exploité cette programmabilité offerte par eBPF pour doter les infrastructures avec des services de supervision, de tracing, et de sécurité de façon native en les exécutant au niveau du noyau. Cela assure des hautes performances et une forte visibilité sur l’activité des applications. La criticité du noyau restreint néanmoins les instructions que peut exécuter un programme eBPF. Le composant responsable de la vérification de la sûreté des programmes est le verifier eBPF. L’objectif du verifier est d’assurer que les programmes qui seront exécutés par le noyau sont sûrs. Cela a pour conséquence de réduire significativement l’expressivité offerte par eBPF en limitant certains mécanismes de programmation comme les boucles de taille de variable, ou encore de limiter le nombre d’instructions que peut exécuter un programme donné. Ces limites rendent le développement d’applications de sécurité complexe comme le traitement de trafic http, ou la gestion de connexions TLS.
 Objectif scientifique - résultats et verrous à lever
L’objectif de la thèse est de reconsidérer la conception de la vérification de programmes telle qu’elle est mise en oeuvre par le verifier eBPF afin d’améliorer la robustesse de la vérification d’une part et d’augmenter l’expressivité des programmes d’autre part.

Compétences (scientifiques et techniques) et qualités personnelles exigées par le poste
-      Architectures des systèmes d’exploitation  
-      Théorie des langages-compilation              
-      Vérification formelle
-      Programmation C                                         
 Formation demandée (master, diplôme d’ingénieur, doctorat, domaine scientifique et technique …)
Master ou diplôme d’ingénieur dans le domaine de l’informatique fondamentale
Expériences souhaitées (stages, …)
Stage en noyau Linux, en langages formels, ou en théorie des langages