| KEYWORD |
DAUIN - GR-03 - COMPUTER NETWORKS GROUP - NETGROUP
Progetto ed implementazione di un verificatore per la compilazione di codice eBPF
Parole chiave ANALISI STATICA, COMPILATORI, EBPF, LINUX
Riferimenti RICCARDO SISTO
Gruppi di ricerca COMPUTER NETWORKS GROUP - NETGROUP, DAUIN - GR-03 - COMPUTER NETWORKS GROUP - NETGROUP, GR-03 - COMPUTER NETWORKS GROUP - NETGROUP, NETGROUP
Tipo tesi SVILUPPO SOFTWARE, TEORICO/SPERIMENTALE
Descrizione eBPF (extended Berkeley Packet Filter) è una tecnologia che può essere usata per installare semplici programmi (plugin) definiti dall'utente nel kernel di linux. eBPF è usato ampiamente per implementare efficientemente packet processing, monitoraggio e tracciamento della sicurezza e altro.
I programmi eBPF sono solitamente scritti in C, quindi compilati in codice eBPF che è infine compilato con compilazione just in time in codice nativo.
Per evitare instabilità del kernel, crash e problemi di security, prima di essere eseguito nel kernel il codice deve passare una verifica, fatta dal verificatore eBPF, un analizzatore statico che rileva i programmi insicuri e pericolosi che devono essere scartati prima del caricamento.
Uno dei problemi che affligge gli sviluppatori di codice eBPF e rende questa programmazione difficoltosa e dispendiosa è che il programmatore può sapere chje un programma non passa la verifica solo quando tenta di caricare il codice, e i messaggi di errore che il verificatore produce sono difficili da capire e da mettere in relazione con il codice sorgente scritto originalmente dal programmatore.
L'obiettivo di questa tesi è di progettare ed implementare un altro verificatore che agisca quando il codice C viene compilato, e che, se il codice non può essere tradotto in un codice che passi la verifica eBPF, ritorni prontamente messaggi di errore facilmente comprensibili e riferibili puntualmente al codice sorgente che causa il problema.
Il verificatore dovrà essere integrato nel compilatore C clang (il frontend di LLVM, solitamente adottato per la compilazione del codice eBPF ), che già offre diversi componenti per costruire analizzatori statici del codice.
La tesi verrà sviluppata nel contesto di un progetto di ricerca europeo che offrirà l'opportunità di interagire con partner di università e aziende europee (per esempio, Ericsson, Telefonica, Thales).
Per lo svolgimento di questa tesi è richiesto un buon curriculum.
Conoscenze richieste Buone abilità di programmazione in C.
Preferibile aver seguito il corso Formal Languages and Compilers.
Scadenza validita proposta 09/01/2025
PROPONI LA TUA CANDIDATURA