On Tue, Mar 19, 2024 at 09:16:25PM +0000, Harishankar Vishwanathan wrote: > 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 Thank you all for working on Agni, and the continue effort to verify the latest codebase! > 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. Q: looking at README in Agni's repo both the 64-bit and 32-bit u/smin u/smax gets verified, is that right? > ...
