bpf-runtime-verifier

Prerequisites

We mainly need z3 to reason about the memory addresses

pip install -r requirements.txt

Usage

Run the program with an ebpf program with a few restrictions:

Program must produce a directed, acyclic graph. This means no loops or unrolled loops. Don't supply an elf object, just the ebpf instructions. See section below for how to do this.

python3 main.py ebpf_object.o

get instructions only from elf format

llvm-objcopy -O binary --only-section=.text program.bpf.o a.o