Running Agni on 6.8

To run Agni on the latest kernel requires a preprocessing step: regs_refine_cond_op has a goto-label that introduces a backwards edge in the control-flow graph of the verifier, something that Agni does not support yet. We provide a patch that essentially removes this backwards edge and makes the verifier code a DAG, while keeping it functionally equivalent. To verify the range analysis in 6.8 and recreate our results (the verifier is sound), one can follow the following steps.

1. Obtain the kernel sources for 6.8
2. Apply this patch and commit it, obtain the commit-ish
3. Clone agni from https://github.com/bpfverif/agni/
4. Install Agni's dependencies, including python >= 3.9.
5. Create a directory for results: /path/to/results
6. Change directory: cd agni
7. Generate SMT encodings for the prefix (everything except reg_bounds_sync) of all BPF operators. Also generate SMT encodings for the suffix (reg_bounds_sync) separately.

python3 llvm-to-smt/generate_encodings.py \
--llvmdir </path/to/llvm-12> \
--outdir </path/to/results> \
--kernbasedir </path/to/linux-6.8-source/> \
--kernver 6.8 \
--commit <patch-commit-ish> \
--modular

8. Verify the prefix of all BPF operators, and verify the suffix (reg_bounds_sync). This is what we call gen verification. If verification fails, precondition the inputs to all abstract operators with the output of reg_bounds_sync. This is what we call sro verification. If both gen verification and sro verification fail, this script will proceed to synthesizing an eBPF program that manifests a bug in the verifier.

python3 bpf-verification/src/bpf_alu_jmp_synthesis.py \
--kernver 6.8 \
--json_offset 3 \
--encodings_path </path/to/results> \
--res_path </path/to/results>