| KEYWORD |
Design and implementation of a verifier for eBPF code compilation
keywords COMPILERS, EBPF, LINUX, STATIC ANALYSIS
Reference persons RICCARDO SISTO
Research Groups COMPUTER NETWORKS GROUP - NETGROUP, DAUIN - GR-03 - COMPUTER NETWORKS GROUP - NETGROUP, GR-03 - COMPUTER NETWORKS GROUP - NETGROUP, NETGROUP
Thesis type SOFTWARE DEVELOPMENT, THEORETICAL/EXPERIMENTAL
Description eBPF (extended Berkeley Packet Filter) is a technology that can be used to install user-defined simple plugin programs into the linux kernel. eBPF is used extensively to implement efficiently packet processing, security monitoring and tracing, and more.
eBPF programs are usually written in C, then compiled to eBPF code, which is finally just in time compiled to native code.
In order to avoid kernel instability, crashes and security issues, before being executed in the kernel the code must pass a verification, done by the eBPF verifier, a static analyzer which detects insecure and dangerous programs to be discarded before loading.
One of the issues that makes eBPF programming challenging and time-consuming is that the programmer can know that a program does not pass the verification only at load time, and the error message produced by the verifier is difficult to understand and to relate to the original source code written by the programmer.
The goal of this thesis work is to design and implement an additional verifier that acts when the C code is compiled, and returns prompt and easy to understand messages related to the source if the code cannot be compiled into a code that passes the eBPF verification.
The verifier has to be integrated into the clang C compiler (the LLVM frontend usually adopted for eBPF compilation), which already offers several building blocks for building static code analyzers.
The thesis will be developed in the context of a European research project, which will give the opportunity to interact with partners from foreign Universities and Companies (e.g., Ericsson, Telefonica, Thales).
For this thesis, a good curriculum is requested, and a scholarship is also available.
Required skills Good C programming skills.
Having taken the Formal Languages and Compilers course is advised.
Deadline 09/01/2025
PROPONI LA TUA CANDIDATURA