Re: Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu <shung-hsi.yu@suse.com>]

On Mon, Oct 23, 2023 at 09:50:59AM -0700, Andrii Nakryiko wrote:
> On Mon, Oct 23, 2023 at 6:14 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> >
> > Hi,
> >
> > CC those who had worked on bound tracking before for feedbacks, as well as
> > Dave who works on PREVAIL (verifier used on Windows) and Paul who've written
> > about PREVAIL[1], for whether there's existing knowledge on this topic.
> >
> > Here goes a long one...
> >
> > ---
> >
> > While looking at Andrii's patches that improves bounds logic (specifically
> > patches [2][3]). I realize we may be able to unify umin/umax/smin/smax into
> > just two u64. Not sure if this has already been discussed off-list or is
> > being worked upon, but I can't find anything regarding this by searching
> > within the BPF mailing list.
> >
> > For simplicity sake I'll focus on unsigned bounds for now. What we have
> > right in the Linux Kernel now is essentially
> >
> >     struct bounds {
> >         u64 umin;
> >         u64 umax;
> >     }
> >
> > We can visualize the above as a number line, using asterisk to denote the
> > values between umin and umax.
> >
> >                  u64
> >     |----------********************--|
> >
> > Say if we have umin = A, and umax = B (where B > 2^63). Representing the
> > magnitude of umin and umax visually would look like this
> >
> >     <----------> A
> >     |----------********************--|
> >     <-----------------------------> B (larger than 2^63)
> >
> > Now if we go through a BPF_ADD operation and adds 2^(64 - 1) = 2^63,
> > currently the verifier will detect that this addition overflows, and thus
> > reset umin and umax to 0 and U64_MAX, respectively; blowing away existing
> > knowledge.
> >
> >     |********************************|
> >
> > Had we used u65 (1-bit more than u64) and tracks the bound with u65_min and
> > u65_max, the verifier would have captured the bound just fine. (This idea
> > comes from the special case mentioned in Andrii's patch[3])
> >
> >                                     u65
> >     <---------------> 2^63
> >                     <----------> A
> >     <--------------------------> u65_min = A + 2^63
> >     |--------------------------********************------------------|
> >     <---------------------------------------------> u65_max = B + 2^63
> >
> > Continue on this thought further, let's attempting to map this back to u64
> > number lines (using two of them to fit everything in u65 range), it would
> > look like
> >
> >                                     u65
> >     |--------------------------********************------------------|
> >                                vvvvvvvvvvvvvvvvvvvv
> >     |--------------------------******|*************------------------|
> >                    u64                              u64
> >
> > And would seems that we'd need two sets of u64 bounds to preserve our
> > knowledge.
> >
> >     |--------------------------******| u64 bound #1
> >     |**************------------------| u64 bound #2
> >
> > Or just _one_ set of u64 bound if we somehow are able to track the union of
> > bound #1 and bound #2 at the same time
> >
> >     |--------------------------******| u64 bound #1
> >   U |**************------------------| u64 bound #2
> >      vvvvvvvvvvvvvv            vvvvvv  union on the above bounds
> >     |**************------------******|
> >
> > However, this bound crosses the point between U64_MAX and 0, which is not
> > semantically possible to represent with the umin/umax approach. It just
> > makes no sense.
> >
> >     |**************------------******| union of bound #1 and bound #2
> >
> > The way around this is that we can slightly change how we track the bounds,
> > and instead use
> >
> >     struct bounds {
> >         u64 base; /* base = umin */
> >         /* Maybe there's a better name other than "size" */
> >         u64 size; /* size = umax - umin */
> >     }
> >
> > Using this base + size approach, previous old bound would have looked like
> >
> >     <----------> base = A
> >     |----------********************--|
> >                <------------------> size = B - A
> >
> > Looking at the bounds this way means we can now capture the union of bound
> > #1 and bound #2 above. Here it is again for reference
> >
> >     |**************------------******| union of bound #1 and bound #2
> >
> > Because registers are u64-sized, they wraps, and if we extend the u64 number
> > line, it would look like this due to wrapping
> >
> >                    u64                         same u64 wrapped
> >     |**************------------******|*************------------******|
> >
> > Which can be capture with the base + size semantic
> >
> >     <--------------------------> base = (u64) A + 2^63
> >     |**************------------******|*************------------******|
> >                                <------------------> size = B - A,
> >                                                     doesn't change after add
> >
> > Or looking it with just a single u64 number line again
> >
> >     <--------------------------> base = (u64) A + 2^63
> >     |**************------------******|
> >     <-------------> base + size = (u64) (B + 2^32)
> >
> > This would mean that umin and umax is no longer readily available, we now
> > have to detect whether base + size wraps to determin whether umin = 0 or
> > base (and similar for umax). But the verifier already have the code to do
> > that in the existing scalar_min_max_add(), so it can be done by reusing
> > existing code.
> >
> > ---
> >
> > Side tracking slightly, a benefit of this base + size approach is that
> > scalar_min_max_add() can be made even simpler:
> >
> >     scalar_min_max_add(struct bpf_reg_state *dst_reg,
> >                                struct bpf_reg_state *src_reg)
> >     {
> >         /* This looks too simplistic to have worked */
> >         dst_reg.base = dst_reg.base + src_reg.base;
> >         dst_reg.size = dst_reg.size + src_reg.size;
> >     }
> >
> > Say we now have another unsigned bound where umin = C and umax = D
> >
> >     <--------------------> C
> >     |--------------------*********---|
> >     <----------------------------> D
> >
> > If we want to track the bounds after adding two registers on with umin = A &
> > umax = B, the other with umin = C and umin = D
> >
> >     <----------> A
> >     |----------********************--|
> >     <-----------------------------> B
> >                      +
> >     <--------------------> C
> >     |--------------------*********---|
> >     <----------------------------> D
> >
> > The results falls into the following u65 range
> >
> >     |--------------------*********---|-------------------------------|
> >   + |----------********************--|-------------------------------|
> >
> >     |------------------------------**|**************************-----|
> >
> > This result can be tracked with base + size approach just fine. Where the
> > base and size are as follow
> >
> >     <------------------------------> base = A + C
> >     |------------------------------**|**************************-----|
> >                                    <--------------------------->
> >                                       size = (B - A) + (D - C)
> >
> > ---
> >
> > Now back to the topic of unification of signed and unsigned range. Using the
> > union of bound #1 and bound #2 again as an example (size = B - A, and
> > base = (u64) A + 2^63)
> >
> >     |**************------------******| union of bound #1 and bound #2
> >
> > And look at it's wrapped number line form again
> >
> >                    u64                         same u64 wrapped
> >     <--------------------------> base
> >     |**************------------******|*************------------******|
> >                                <------------------> size
> >
> > Now add in the s64 range and align both u64 range and s64 at 0, we can see
> > what previously was a bound that umin/umax cannot track is simply a valid
> > smin/smax bound (idea drawn from patch [2]).
> >
> >                                      0
> >     |**************------------******|*************------------******|
> >                     |----------********************--|
> >                                     s64
> >
> > The question now is be what is the "signed" base so we proceed to calculate
> > the smin/smax. Note that base starts at 0, so for s64 the line that
> > represents base doesn't start from the left-most location.
> > (OTOH size stays the same, so we know it already)
> >
> >                                     s64
> >                                      0
> >                                <-----> signed base = ?
> >                     |----------********************--|
> >                                <------------------> size is the same
> >
> > If we put u64 range back into the picture again, we can see that the "signed
> > base" was, in fact, just base casted into s64, so there's really no need for
> > a "signed" base at all
> >
> >     <--------------------------> base
> >     |**************------------******|
> >                                      0
> >                                <-----> signed base = (s64) base
> >                     |----------********************--|
> >
> > Which shows base + size approach capture signed and unsigned bounds at the
> > same time. Or at least its the best attempt I can make to show it.
> >
> > One way to look at this is that base + size is just a generalization of
> > umin/umax, taking advantage of the fact that the similar underlying hardware
> > is used both for the execution of BPF program and bound tracking.
> >
> > I wonder whether this is already being done elsewhere, e.g. by PREVAIL or
> > some of static code analyzer, and I can just borrow the code from there
> > (where license permits).
> 
> A slight alternative, but the same idea, that I had (though after
> looking at reg_bounds_sync() I became less enthusiastic about this)
> was to unify signed/unsigned ranges by allowing umin u64> umax. That
> is, invalid range where umin is greater than umax would mean the wrap
> around case (which is also basically smin/smax case when it covers
> negative and positive parts of s64/s32 range).
> 
> Taking your diagram and annotating it a bit differently:
> 
> |**************------------******|
>              umax        umin

Yes, that was exactly that's how I look at it at first (not that
surprisingly given I was drawing ideas from you patchset :) ), and it
certainly has the benefit of preserving both bounds, where as the base +
size approach only preserve one of the bounds, leaving the other to be
calculated.

The problem I have with allowing umin u64> umax is mostly a naming one, that
it would be rather error prone and too easy to assume umin is always smaller
than umax (after all, that how it works now); and I can't come up with a
better name for them in that form.

But as you've pointed out both approach are the same idea, if one works so
will the other.

> It will make everything more tricky, but if someone is enthusiastic
> enough to try it out and see if we can make this still understandable,
> why not?

I'll blindly assume reg_bounds_sync() can be worked out eventually to keep
my enthusiasm and look at just the u64/s64 case for now, let see how that
goes...

> > The glaring questions left to address are:
> > 1. Lots of talk with no code at all:
> >      Will try to work on this early November and send some result as RFC. In
> >      the meantime if someone is willing to give it a try I'll do my best to
> >      help.
> >
> > 2. Whether the same trick applied to scalar_min_max_add() can be applied to
> >    other arithmetic operations such as BPF_MUL or BPF_DIV:
> >      Maybe not, but we should be able to keep on using most of the existing
> >      bound inferring logic we have scalar_min_max_{mul,div}() since base +
> >      size can be viewed as a generalization of umin/umax/smin/smax.
> >
> > 3. (Assuming this base + size approach works) how to integrate it into our
> >    existing codebase:
> >      I think we may need to refactor out code that touches
> >      umin/umax/smin/smax and provide set-operation API where possible. (i.e.
> >      like tnum's APIs)
> >
> > 4. Whether the verifier loss to ability to track certain range that comes
> >    out of mixed u64 and s64 BPF operations, and this loss cause some BPF
> >    program that passes the verfier to now be rejected.
> 
> Very well might be, I've seen some crazy combinations in my testing.
> Good thing is that I'm adding a quite exhaustive tests that try all
> different boundary conditions. If you check seeds values I used, most
> of them are some sort of boundary for signed/unsigned 32/64 bit
> numbers. Add to that abstract interpretation model checking, and you
> should be able to validate your ideas pretty easily.

Thanks for the heads up. Would be glad to see the exhaustive tests being
added!

> > 5. Probably more that I haven't think of, feel free to add or comments :)
> >
> >
> > Shung-Hsi
> >
> > 1: https://pchaigno.github.io/ebpf/2023/09/06/prevail-understanding-the-windows-ebpf-verifier.html
> > 2: https://lore.kernel.org/bpf/20231022205743.72352-2-andrii@kernel.org/
> > 3: https://lore.kernel.org/bpf/20231022205743.72352-4-andrii@kernel.org/