Re: [PATCH bpf-next v5 4/5] bpf: verifier: Support eliding map lookup nullness

[Alexei Starovoitov]

On Thu, Dec 19, 2024 at 4:43 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Thu, 2024-12-19 at 17:40 -0700, Daniel Xu wrote:
>
> [...]
>
> > > Ok, thinking a bit more, the best test I can come up with is:
> > >
> > >   u8 vals[8];
> > >   vals[0] = 0;
> > >   ...
> > >   vals[6] = 0;
> > >   vals[7] = 0xf;
> > >   p = bpf_map_lookup_elem(... vals ...);
> > >   *p = 42;
> > >
> > > For LE vals as u32 should be 0x0f;
> > > For BE vals as u32 should be 0xf000_0000.
> > > Hence, it is not safe to remove null check for this program.
> > > What would verifier think about the value of such key?
> > > As far as I understand, there would be stack zero for for vals[0-6]
> > > and u8 stack spill for vals[7].
> >
> > Right. By checking that spill size is same as key size, we stay endian
> > neutral, as constant values are tracked in native endianness.
> >
> > However, if we were to start interpreting combinations of STACK_ZERO,
> > STACK_MISC, and STACK_SPILL, the verifier would have to be endian aware
> > (IIUC). Which makes it a somewhat interesting problem but also requires
> > some thought to correctly handle the state space.
>
> Right.
>
> > > You were going to add a check for the spill size, which should help here.
> > > So, a negative test like above that checks that verifier complains
> > > that 'p' should be checked for nullness first?
> > >
> > > If anyone has better test in mind, please speak-up.
> >
> > I think this case reduces down to a spill_size != key_size test. As long
> > as the sizes match, we don't have to worry about endianness.
>
> Agree.

Earlier I suggested to generalize this zero/misc/spill counting
into a helper and reuse here and in check_stack_read_fixed_off().

We do very similar checks there with a similar purpose.

It sounds there are ideas to make this particular feature smarter
than what we have in check_stack_read_fixed_off().
Let's not overdo it.
Even if a common helper is not possible, keep things consistent.
The simpler the better.