10 — bpf(): the verifier

The kernel runs programs supplied from user space inside itself. What convinces it that’s safe, and what does the proof look like?

Requirements: the guest from chapter 7, and comfort reading C.

The path

Step 1: load. __sys_bpf calls bpf_prog_load (kernel/bpf/syscall.c), which copies the instructions, records whether the licence is GPL-compatible, and calls bpf_check. Rejecting GPL-only helpers happens later, in check_helper_call.

Step 2: static checks. bpf_check (kernel/bpf/verifier.c) runs passes in this order (verifier.c): check_btf_info_early, add_subprog_and_kfunc, check_subprogs, check_btf_info, check_attach_btf_id, resolve_pseudo_ldimm64, check_cfg, mark_fastcall_patterns, then do_check_main and do_check_subprogs, then fixups.

check_cfg walks the control-flow graph. It rejects back-edges only for loaders without CAP_BPF. It doesn’t prove loops terminate.

Step 3: symbolic execution. do_check is the proof, and termination is shown here. It explores every path. For each instruction, every register has a bpf_reg_state:

• a type: SCALAR_VALUE, PTR_TO_CTX, PTR_TO_MAP_VALUE, PTR_TO_PACKET, PTR_TO_STACK and so on
• for scalars, a tnum of known bits, plus signed and unsigned min and max bounds, refined by every comparison

Memory accesses are checked against the pointer’s type and bounds. Helper calls are checked against their prototypes. Context accesses go through the program type’s is_valid_access.

Step 4: pruning. At each branch, one state is pushed with push_stack and both arms are explored. is_state_visited stops re-exploring a state that’s a subset of one already proven safe (verifier docs). There’s a limit of 1,000,000 processed instructions (bpf.h).

Step 5: kfuncs. Programs can call kernel functions as well as helpers. Kfuncs are registered per program type and “do not have a stable interface” (kfuncs docs).

Step 6: rewrite and compile. convert_ctx_accesses turns context fields into real offsets, and do_misc_fixups patches helper calls. bpf_prog_select_runtime calls the JIT, bpf_int_jit_compile in arch/x86/net/bpf_jit_comp.c.

Step 7: attach. link_create or bpf_prog_attach take over, by type. (bpf_link_create is libbpf’s name, not the kernel’s.) cgroup_bpf_attach is one of the paths, covered in chapter 11.

Hands-on: argue with the verifier

1. Create xdp_bad.bpf.c. It reads a packet with no bounds check unless FIXED is set:

   #include "vmlinux.h"
   #include <bpf/bpf_helpers.h>
   
   SEC("xdp")
   int xdp_bad(struct xdp_md *ctx)
   {
       unsigned char *data = (void *)(long)ctx->data;
   #ifdef FIXED
       void *data_end = (void *)(long)ctx->data_end;
       if ((void *)(data + 21) > data_end)
           return XDP_DROP;
   #endif
       return data[20] == 0xff ? XDP_DROP : XDP_PASS;
   }
   char LICENSE[] SEC("license") = "GPL";

2. Load the bad version and read the log:

   clang -O2 -g -target bpf -c xdp_bad.bpf.c -o bad.o
   bpftool -d prog load bad.o /sys/fs/bpf/bad 2>&1 | less

3. Look for: a rejection about invalid packet access, showing the register’s offset and range. Read each field.

4. Load the fixed version:

   clang -O2 -g -target bpf -DFIXED -c xdp_bad.bpf.c -o fixed.o
   bpftool -d prog load fixed.o /sys/fs/bpf/fixed 2>&1 | less

5. Expected: after the branch, the packet pointer should show r=21, and the log should end with a processed N insns line. The comparison gave the verifier the proof it needed.

Always compile with -O2, because -O0 output tends to be rejected. Delete pinned files between runs.

Hands-on: see what it became

1. Compare the rewritten and compiled forms:

   bpftool prog dump xlated pinned /sys/fs/bpf/fixed
   bpftool prog dump jited pinned /sys/fs/bpf/fixed

   The second needs bpftool built with libbfd or LLVM support.

2. Trace the verifier itself:

   bpftrace -e 'kprobe:bpf_check,kprobe:do_check,kprobe:is_state_visited,kprobe:bpf_int_jit_compile { @[probe]=count(); }'

   Look for: how often pruning is consulted for one program.

3. See the load sequence:

   bpftrace -e 'tracepoint:syscalls:sys_enter_bpf { printf("%s cmd=%d\n", comm, args.cmd); }'

   Match the numbers against enum bpf_cmd. Expect commands like BPF_BTF_LOAD, BPF_MAP_CREATE, BPF_PROG_LOAD and BPF_LINK_CREATE.

Hands-on: two more rejections

1. The most common one. Add a map lookup and dereference the result with no NULL check. Find the invalid mem access message, add the check, and reload.
2. Loops. As root, write a loop that can’t terminate. Expect infinite loop detected or BPF program is too large, not a back-edge message, because root is bpf_capable (verifier.c). The compiler may remove a silly loop, so check the output with llvm-objdump -d.

The takeaway

Safety by proof, not by trust. The verifier doesn’t sandbox the program at runtime; it refuses to run anything it can’t prove safe in advance, by tracking what every register could contain along every path. The cost is a restricted language and sometimes an argument with the prover; the payoff is execution with no runtime checks for those properties. The design question it poses to you (can I verify this before I run it, instead of guarding it while it runs?) is worth asking of every plugin system, every rules engine and every “let the customer upload code” feature.