Re: [PATCH v5 bpf-next 00/23] BPF register bounds logic and testing improvements

Andrii Nakryiko
2023-10-31T05:19:25Z

On Mon, Oct 30, 2023 at 10:55 AM Alexei Starovoitov
<alexei.starovoitov@gmail.com> 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@mail.gmail.com/
>
> 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!)