On Tue, Mar 19, 2024 at 2:16 PM Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxxxx> wrote: > > 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 Nice, great to have this verified, thanks! > 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
