eBPF-SE
eBPF symbolic execution tool
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.
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.
active
—
entered showcase: 2024-03-20
—
entry updated: 2024-03-20
This project has not yet been evaluated by the C4DT Factory team.
We will be happy to evaluate it upon request.
Application
C
MIT