Thèse - Extension du noyau Linux par des programmes utilisateurs sûrs - F/H

votre rôle

 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 œuvre 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.

Il est attendu des résultats de la thèse une confrontation des choix de vérification adoptés par la communauté Linux à l’état de l’art de la vérification formelle d’une part et à celui des langages de programmation dits sûrs comme Rust d’autre part pour proposer une amélioration de l’utilisabilité de l’infrastructure eBPF. Un résultat subsidiaire de la thèse serait de réduire le recours aux helpers (fonctions du noyau Linux).