This repository hosts eBPF-SE, a tool that can be used to symbolically execute programs written using the Linux kernel's eBPF framework. eBPF-SE was previously a part of PIX, a tool that automatically extracts performance interfaces from NF code. In case eBPF-SE is useful to you in any published work, please cite the PIX paper published at NSDI'22.

Subdirectories have their own README files.

• examples - contains a set of example eBPF programs that eBPF-SE has been used to symbolically execute so far.
• tool - contains the symbolic execution engine which is based on KLEE
• libbpf-stubbed - Simple models (stubs) for the Linux kernel's libbpf API that are amenable to symbolic execution. Linking against these models (as opposed to the real implementation of these API functions in the Linux kernel) ensures that eBPF-SE can explore all program paths through the loaded eBPF program without running into path explosion. Current directory is up-to-date with libbpf 1.2.2.

First, setup the tool as follows:

cd tool
./setup-tool.sh
source paths.sh

This step should take approximately 10 minutes and will install the symbolic execution engine along with all of its dependencies (KLEE, klee-uclibc and Z3). This also creates a paths.sh file which contains commands to add klee and its include directory to your path. We recommend adding source ebpf-se/tool/paths.sh to your .bashrc for ease of use.

Then, to test the tool on any of the provided examples (for instance, Katran):

cd examples/katran  # Replace with example of your choice here
make libbpf # This needs to be done only for the first example you run
make xdp-target
make symbex

You should automatically see the KLEE output at the end of third step, which describes the total number of paths explored during symbolic execution. The analysis for Katran, which is one of the more complex eBPF programs, takes approximately 2 minutes and yields 16110 paths.

Please follow the steps listed in examples/README.md.

• All code in this repository was tested on Ubuntu 22.04.