On Mon, Oct 30, 2023 at 10:55 AM Alexei Starovoitov <alexei.starovoitov@xxxxxxxxx> wrote: > > On Fri, Oct 27, 2023 at 11:13:23AM -0700, Andrii Nakryiko wrote: > > > > Note, this is not unique to <range> vs <range> logic. Just recently ([0]) > > a related issue was reported for existing verifier logic. This patch set does > > fix that issues as well, as pointed out on the mailing list. > > > > [0] https://lore.kernel.org/bpf/CAEf4Bzbgf-WQSCz8D4Omh3zFdS4oWS6XELnE7VeoUWgKf3cpig@xxxxxxxxxxxxxx/ > > Quick comment regarding shift out of bound issue. > I think this patch set makes Hao Sun's repro not working, but I don't think > the range vs range improvement fixes the underlying issue. Correct, yes, I think adjust_reg_min_max_vals() might still need some fixing. > Currently we do: > if (umax_val >= insn_bitness) > mark_reg_unknown > else > here were use src_reg->u32_max_value or src_reg->umax_value > I suspect the insn_bitness check is buggy and it's still possible to hit UBSAN splat with > out of bounds shift. Just need to try harder. > if w8 < 0xffffffff goto +2; > if r8 != r6 goto +1; > w0 >>= w8; > won't be enough anymore. Agreed, but I felt that fixing adjust_reg_min_max_vals() is out of scope for this already large patch set. If someone can take a deeper look into reg bounds for arithmetic operations, it would be great. On the other hand, one of those academic papers claimed to verify soundness of verifier's reg bounds, so I wonder why they missed this? cc Paul, maybe he can clarify (and also, Paul, please try to run all that formal verification machinery against this patch set, thanks!)
