Re: [PATCH bpf-next v5 15/25] bpf: Teach verifier about non-size constant arguments

[Kumar Kartikeya Dwivedi <memxor@gmail.com>]

On Wed, Nov 09, 2022 at 05:35:26AM IST, Andrii Nakryiko wrote:
> On Mon, Nov 7, 2022 at 3:10 PM Kumar Kartikeya Dwivedi <memxor@gmail.com> wrote:
> >
> > Currently, the verifier has support for various arguments that either
> > describe the size of the memory being passed in to a helper, or describe
> > the size of the memory being returned. When a constant is passed in like
> > this, it is assumed for the purposes of precision tracking that if the
> > value in the already explored safe state is within the value in current
> > state, it would fine to prune the search.
> >
> > While this holds well for size arguments, arguments where each value may
> > denote a distinct meaning and needs to be verified separately needs more
> > work. Search can only be pruned if both are equivalent values. In all
> > other cases, it would be incorrect to treat those two precise registers
> > as equivalent if the new value satisfies the old one (i.e. old <= cur).
> >
> > Hence, make the register precision marker tri-state. There are now three
> > values that reg->precise takes: NOT_PRECISE, PRECISE, EXACT.
> >
> > Both PRECISE and EXACT are 'true' values. EXACT affects how regsafe
> > decides whether both registers are equivalent for the purposes of
> > verifier state equivalence. When it sees that old state register has
> > reg->precise == EXACT, unless both are equivalent, it will return false.
> > Otherwise, for PRECISE case it falls back to the default check that is
> > present now (i.e. thinking that we're talking about sizes).
> >
> > This is required as a future patch introduces a BPF memory allocator
> > interface, where we take the program BTF's type ID as an argument. Each
> > distinct type ID may result in the returned pointer obtaining a
> > different size, hence precision tracking is needed, and pruning cannot
> > just happen when the old value is within the current value. It must only
> > happen when the type ID is equal. The type ID will always correspond to
> > prog->aux->btf hence actual type match is not required.
> >
> > Finally, change mark_chain_precision precision argument to EXACT for
> > kfuncs constant non-size scalar arguments (tagged with __k suffix).
> >
> > Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
> > ---
>
> I think this needs a bit more thinking, tbh. First, with my recent
> changes we don't even set precision marks in current state, everything
> stays imprecise. And then under CAP_BPF we also aggressively reset
> precision. This might work for EXACT, but needs careful consideration.
>

I'm sorry, I didn't have the time to look at the series, but I spent the whole
day going over it today, and it makes a lot of sense to me. I think I also
misunderstood some things and going through it brought some clarity.

I think resetting precision is fine here too. As you've stated in that series,
the verifier while simulating execution in current state already checks
everything.

> But, taking a step back. I'm trying to understand why this whole EXACT
> mode is necessary. SCALAR has min/max values which regsafe() does
> check. So for those special ___k arguments, if we correctly set
> min/max values to be *exactly* the btf_id passed in, why would
> regsafe()'s logic not work?
>

Yes, when you have tnum_is_const var_off, regsafe will return false (when
reg->precise is true). So EXACT is unnecessary in that case.

I think you're probably right. The range_within will fail for k1 != k2,
but I was more concerned for cases where it's not a constant made a concrete
value later.

rX = ...; [X1, Y1];
if (cond) // unknown
  rX = ...; [X2, Y2];
p:
...

p is a pruning point, so states will be compared there. I spent a fair amount of
time today trying to break this in different ways but failed so far. Also,
thinking about if it still lies within that range, things should still be ok
since it's in the same admissible set of values for the scalar that was later
refined and used as a constant for bpf_obj_new. So it's probably unncessary to
make things more pessimistic. The verifier will ensure the current value is
always a subset of the old value.

I guess I'll hold on for this patch and work towards getting the rest in first
(since Alexei mentioned others are waiting on this), and circle back to this if
I am able to construct a real test case that breaks. bpf_obj_new is already
behind CAP_BPF.