PREVAIL - A new eBPF verifier

a Polynomial-Runtime EBPF Verifier using an Abstract Interpretation Layer

The version discussed in the PLDI paper is available here.

DeepWiki: A comprehensive auto-generated documentation is avaliable at https://deepwiki.com/vbpf/prevail

Getting Started

Clone:

git clone --recurse-submodules https://github.com/vbpf/prevail.git
cd prevail

Building

🐧 Linux

Dependencies (Ubuntu)

Prevail is built as C++23, which requires GCC 13+ or Clang 17+. The default toolchain on Ubuntu 24.04 LTS (build-essential → GCC 13) is sufficient. On Ubuntu 22.04 install g++-13 from the ubuntu-toolchain-r PPA; the default GCC 11 will not build the project. Earlier Ubuntu releases (e.g. 20.04) are not supported.

sudo apt install build-essential git cmake libboost-dev libyaml-cpp-dev
sudo apt install libboost-filesystem-dev libboost-program-options-dev

Make

cmake -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build

🪟 Windows

Dependencies

Install git
Install Visual Studio Build Tools 2022 and:
- Choose the “C++ build tools” workload (Visual Studio Build Tools 2022 has support for CMake Version 3.25)
- Under Individual Components, select:
  - “C++ Clang Compiler”
  - “MSBuild support for LLVM”
Install nuget.exe

Make on Windows (which uses a multi-configuration generator)

cmake -B build
cmake --build build --config Release

🍏 macOS

Dependencies:

brew install llvm cmake boost yaml-cpp

The system LLVM (shipped with Xcode Command Line Tools) provides Clang 15, which isn’t enough to compile prevail since it depends on C++23. Brew’s LLVM comes with Clang 17 (or newer), which has sufficient C++23 support.

Make:

export CPATH=$(brew --prefix)/include LIBRARY_PATH=$(brew --prefix)/lib CMAKE_PREFIX_PATH=$(brew --prefix)
cmake -B build -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=$(brew --prefix llvm)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm)/bin/clang++
cmake --build build

🐋 Docker

Build and run

docker build -t prevail .
docker run -it prevail ebpf-samples/cilium/bpf_lxc.o 2/1

Example:

$ bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1
PASS: 2/1

Usage

PREVAIL is a new eBPF verifier based on abstract interpretation.


bin/prevail [OPTIONS] path [section] [function]


POSITIONALS:
  path TEXT:FILE REQUIRED     Elf file to analyze
  section SECTION             Section to analyze
  function FUNCTION           Function to analyze

OPTIONS:
  -h,     --help              Print this help message and exit
          --version           Display program version information and exit
          --section SECTION   Section to analyze
          --function FUNCTION Function to analyze
  -l                          List programs
  -q,     --quiet             No stdout output, exit code only
          --cfg               Print control-flow graph and exit

Features:
          --termination, --no-verify-termination{false}
                              Verify termination. Default: ignore
          --allow-division-by-zero, --no-division-by-zero{false}
                              Handling potential division by zero. Default: allow
  -s,     --strict            Apply additional checks that would cause runtime failures
          --stack-size INT:INT in [1 - 1048576]
                              Per-subprogram stack frame size in bytes (default: 512)
          --max-call-stack-frames INT:INT in [1 - 128]
                              Maximum number of nested function calls (default: 8)
          --max-packet-size INT:INT in [1 - 1073741824]
                              Maximum packet size in bytes (default: 65535)
          --include_groups GROUPS:{atomic32,atomic64,base32,base64,callx,divmul32,divmul64,packet}
                              Include conformance groups
          --exclude_groups GROUPS:{atomic32,atomic64,base32,base64,callx,divmul32,divmul64,packet}
                              Exclude conformance groups

Verbosity:
          --simplify, --no-simplify{false}
                              Simplify the display of the CFG by merging chains of instructions
                              into a single basic block. Default: enabled (disabled with
                              --failure-slice)
          --line-info         Print line information
          --print-btf-types   Print BTF types
  -v                          Print invariants and first failure
  -f                          Print first failure
          --failure-slice     Print minimal failure slices showing only instructions that
                              contributed to errors
          --failure-slice-depth UINT
                              Maximum backward steps for failure slicing (default: 200)

CFG output:
          --asm FILE          Print disassembly to FILE
          --dot FILE          Export control-flow graph to dot FILE

A standard alternative to the –asm flag is llvm-objdump -S FILE.

The cfg can be viewed using dot and the standard PDF viewer:

sudo apt install graphviz
bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1 --dot cfg.dot
dot -Tpdf cfg.dot > cfg.pdf