Hi Harishankar, On Sun, Jul 28, 2024 at 06:38:40PM GMT, Harishankar Vishwanathan wrote: > On Tue, Jul 16, 2024 at 10:52 AM Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> wrote: > > This commit teach the BPF verifier how to infer signed ranges directly > > from signed ranges of the operands to prevent verifier rejection, which > > is needed for the following BPF program's no-alu32 version, as shown by > > Xu Kuohai: [...] > Apologies for the late response and thank you for CCing us Shung-Hsi. > > The patch itself seems well thought out and looks correct. Great work! Thanks! :) > We quickly checked your patch using Agni [1], and were not able to find any > violations. That is, given well-formed register state inputs to > adjust_scalar_min_max_vals, the new algorithm always produces sound outputs > for the BPF_AND (both 32/64) instruction. That is great to hear and really boost the level of confidence. Though I did made an update[1] to the patch such that implementation of negative_bit_floor() is change from v &= v >> 1; v &= v >> 2; v &= v >> 4; v &= v >> 8; v &= v >> 16; v &= v >> 32; return v; to one that closer resembles tnum_range() u8 bits = fls64(~v); /* find most-significant unset bit */ u64 delta; /* special case, needed because 1ULL << 64 is undefined */ if (bits > 63) return 0; delta = (1ULL << bits) - 1; return ~delta; My understanding is that the two implementations should return the same output for the same input, so overall the deduction remains the same. And my simpler test with Z3 does not find violation in the new implementation. But it would be much better if we can have Agni check the new implementation for violation as well. Speak of which, would you and others involved in checking this patch be comfortable with adding a formal acknowledgment[2] for the patch so this work can be credited in the git repo as well? (i.e. usually replying with an Acked-by, other alternatives are Reviewed-by and Tested-by) IMHO the work done here is in the realm of Reviewed-by, but that itself comes with other implications[3], which may or may not be wanted depending on individual's circumstances. I'll probably post the updated patch out next week, changing only the comments in [1]. > It looks like you already performed tests with Z3, and Eduard performed a > brute force testing using 6-bit integers. Agni's result stands as an > additional stronger guarantee because Agni generates SMT formulas directly > from the C source code of the verifier and checks the correctness in Z3 > without any external library functions, it uses full 64-bit size bitvectors > in the formulas generated and considers the correctness for 64-bit integer > inputs, and finally it considers the correctness of the *final* output > abstract values generated after running update_reg_bounds() and > reg_bounds_sync(). I had some vague ideas that Agni provides better guarantee, but did not know exactly what they are. Thanks for the clear explanation on the additional guarantee Agni provides; its especially assuring to know that update_reg_bounds() and reg_bounds_sync() have been taken into account. > Using Agni's encodings we were also quickly able to check the precision of > the new algorithm. An algorithm is more precise if it produces tighter > range bounds, while being correct. We are happy to note that the new > algorithm produces outputs that are at least as precise or more precise > than the old algorithm, for all well-formed register state inputs. That is great to hear as well. I really should try Agni myself, hope I could find time in the near future. Cheers, Shung-Hsi 1: https://lore.kernel.org/bpf/20240719081702.137173-1-shung-hsi.yu@xxxxxxxx/ 2: https://www.kernel.org/doc/html/v6.9/process/submitting-patches.html#when-to-use-acked-by-cc-and-co-developed-by 3: https://www.kernel.org/doc/html/v6.9/process/submitting-patches.html#reviewer-s-statement-of-oversight
