Name:
eBPF-SE
Description:
eBPF symbolic execution tool
Professor — Lab:
George CandeaDependable Systems Lab

Layman description:
eBPF-SE is a tool that analyzes programs written for the Linux kernel's eBPF framework. It systematically explores all possible execution paths through the program by using symbolic values instead of concrete inputs. This allows finding bugs or verifying properties of the program. eBPF-SE uses models of the Linux APIs to avoid getting bogged down in the real kernel code. It was originally part of a tool for optimizing network software performance.
Technical description:
eBPF-SE is a tool that symbolically executes eBPF programs written for the Linux kernel. It is based on the KLEE symbolic execution engine and uses models (stubs) for the Linux kernel's libbpf API. This allows exploring all program paths without path explosion from the real API implementation. eBPF-SE was previously part of PIX, a tool that extracts performance interfaces from network function code.
Project status:
active — entered showcase: 2024-03-20 — entry updated: 2024-03-20

Source code:
Lab Github - last commit: 2024-03-05
Code quality:
This project has not yet been evaluated by the C4DT Factory team. We will be happy to evaluate it upon request.
Project type:
Application
Programming language:
C
License:
MIT