Hi, We wanted to give you an update on our recent results with verifying the soundness of the latest patches (Re: "BPF register bounds logic and testing improvements”) to the eBPF verifier’s range analysis using our tool Agni [1]. Specifically, we checked the range analysis in the functions adjust_scalar_min_max_vals and descendants (for arithmetic and logic instructions) and reg_set_min_max and descendants (for branching instructions). We were able to confirm that the range analyses in kernel 6.8 is sound, with the following assumptions: we only consider parts of the verifier concerned with range analysis (that is, the part that updates u/smin, u/smax, and tnums in bpf_reg_state), we only consider scalar types (SCALAR_VALUE) in bpf registers, we assume Agni's translation of the verifier's C code to logic (SMT) is correct. Starting from kernel v6.4 onwards, Agni used to take several days to verify these kernels. Further investigation revealed that this was due to the changes to reg_bounds_sync and descendants, which introduced a lot more control flow (branches) in the verifier code, causing a symbolic path explosion that degraded the performance of the verification. To address this, we adopted a modular approach to verification. Consider adjust_scalar_min_max_vals, it can be split as a prefix <X> (adjust_scalar_min_max_vals minus reg_bounds_sync) and a suffix <Y> (reg_bounds_sync), such such that the entire function is represented as <X>.<Y> We were able to verify <X>: assuming that when <X> starts in any well-formed abstract state, <X> will only produce well-formed output states. Similarly we were also able to verify <Y>: assuming that when <Y> starts in any well-formed abstract state, <Y> will only produce well-formed output states. Hence, the entire function <X>.<Y> is sound. In earlier kernel versions, we have found that this modular soundness property is untrue. However, in kernels 6.4 through 6.8, modular soundness holds, making it easier to scale verification by breaking up the monolithic verification task: since <Y> consumes the output of <X>, the full chain of operations <X> followed by <Y> must also be sound. To run Agni on the latest kernels requires a preprocessing step because 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. The patch and the instructions to recreate our results are available at [2]. Best, Harishankar Vishwanathan [1] Agni: https://github.com/bpfverif/agni/ [2] Instructions: https://github.com/bpfverif/agni/wiki/Running-Agni-on-6.8
