Unifying signed and unsigned min/max tracking

Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

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).

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.

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/

Re: Unifying signed and unsigned min/max tracking

[Andrii Nakryiko]

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


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?


>
> 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.

>
> 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/

Re: Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

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/

Re: Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

On Mon, Oct 23, 2023 at 09:14:08PM +0800, Shung-Hsi Yu 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).

As per [1], PREVAIL uses the zone domain[2][3] to track values along with
relationships between values, where as the Linux Kernel tracks values with
min/max (i.e. interval domain) and tnum. In short, PREVAIL does not use this
trick, but I guess it probably don't need to since it's already using
something that considered to be more advanced.

Also, found some research papers on this topic referring to it as Wrapped
Intervals[4] or Modular Interval Domain[5]. The former has an MIT-licensed
C++ implementation[6] available as reference.

1: https://pchaigno.github.io/ebpf/2023/09/06/prevail-understanding-the-windows-ebpf-verifier.html
2: https://en.wikipedia.org/wiki/Difference_bound_matrix#Zone
3: https://github.com/vbpf/ebpf-verifier/blob/6d5ad53/src/crab/split_dbm.hpp
4: https://dl.acm.org/doi/abs/10.1145/2651360
5: https://hal.science/hal-00748094/document
6: https://github.com/caballa/wrapped-intervals/blob/master/lib/RangeAnalysis/WrappedRange.cpp

> 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.
> 
> 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/

Re: Unifying signed and unsigned min/max tracking

[Andrii Nakryiko]

On Thu, Oct 26, 2023 at 10:44 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> On Mon, Oct 23, 2023 at 09:14:08PM +0800, Shung-Hsi Yu 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).
>
> As per [1], PREVAIL uses the zone domain[2][3] to track values along with
> relationships between values, where as the Linux Kernel tracks values with
> min/max (i.e. interval domain) and tnum. In short, PREVAIL does not use this
> trick, but I guess it probably don't need to since it's already using
> something that considered to be more advanced.

tnum is actually critical for checking memory alignment (i.e.,
checking that low 2-3 bits are always zero), which range tracking
can't do. So I suspect PREVAIL doesn't validate those conditions,
while kernel's verifier does.

>
> Also, found some research papers on this topic referring to it as Wrapped
> Intervals[4] or Modular Interval Domain[5]. The former has an MIT-licensed
> C++ implementation[6] available as reference.
>
> 1: https://pchaigno.github.io/ebpf/2023/09/06/prevail-understanding-the-windows-ebpf-verifier.html
> 2: https://en.wikipedia.org/wiki/Difference_bound_matrix#Zone
> 3: https://github.com/vbpf/ebpf-verifier/blob/6d5ad53/src/crab/split_dbm.hpp
> 4: https://dl.acm.org/doi/abs/10.1145/2651360

this one (judging by the name of the paper) looks exactly like what we
are trying to do here. I'll give it a read some time later. Meanwhile
I posted full patch set with range logic ([0]), feel free to take a
look as well.

  [0] https://patchwork.kernel.org/project/netdevbpf/list/?series=797178&state=*

> 5: https://hal.science/hal-00748094/document
> 6: https://github.com/caballa/wrapped-intervals/blob/master/lib/RangeAnalysis/WrappedRange.cpp
>
> > 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.
> >
> > 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/

Re: Unifying signed and unsigned min/max tracking

[Andrii Nakryiko]

On Thu, Oct 26, 2023 at 9:57 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
>
> 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.

min64/max64 and min32/max32 would be my proposal if/when we unify them.

>
> 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...
>

probably, yes


> > > 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!

Check [0]. You can run range vs consts (7.7mln cases) with

sudo SLOW_TESTS=1 ./test_progs -a 'reg_bounds_gen_consts*' -j

And range vs range (106mln cases right now) with

sudo SLOW_TESTS=1 ./test_progs -a 'reg_bounds_gen_ranges*' -j

The latter might take a bit, it runs for about 1.5 hours for me.

It's not exhaustive in a strict sense of this word, as we can't really
try all possible u64/s64 ranges, ever. But it tests a lot of edge
values on the border between min/max values for u32/s32 and u64/s32.
Give it a try.

  [0] https://patchwork.kernel.org/project/netdevbpf/list/?series=797178&state=*

>
> > > 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/

Re: Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

On Fri, Oct 27, 2023 at 01:49:34PM -0700, Andrii Nakryiko wrote:
> On Thu, Oct 26, 2023 at 9:57 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > On Mon, Oct 23, 2023 at 09:50:59AM -0700, Andrii Nakryiko wrote:

[...]

> > > > 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.

[...]

> > > > 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.
> 
> min64/max64 and min32/max32 would be my proposal if/when we unify them.

i'm going with start/end for now since it go along quite well with the
number line analogy, where the number line start at at one point and
ends at another; and it should be less assuming about how the values
compares.

Following this logic, `end - start` would be call the length, rather
than size that I've proposed above. Calling size is not that great
because it implies this is the number of values between the two bounds,
but in fact it is off by one, (borrowing from Eduard's email[1]) the
actual number of values N between two bounds is 

  N = end - start + 1

1: https://lore.kernel.org/bpf/d7af631802f0cfae20df77fe70068702d24bbd31.camel@gmail.com/

> > 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...
> >
> 
> probably, yes
> 
> > > > 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!
> 
> Check [0]. You can run range vs consts (7.7mln cases) with
> 
> sudo SLOW_TESTS=1 ./test_progs -a 'reg_bounds_gen_consts*' -j
> 
> And range vs range (106mln cases right now) with
> 
> sudo SLOW_TESTS=1 ./test_progs -a 'reg_bounds_gen_ranges*' -j
> 
> The latter might take a bit, it runs for about 1.5 hours for me.
> 
> It's not exhaustive in a strict sense of this word, as we can't really
> try all possible u64/s64 ranges, ever. But it tests a lot of edge
> values on the border between min/max values for u32/s32 and u64/s32.
> Give it a try.
> 
>   [0] https://patchwork.kernel.org/project/netdevbpf/list/?series=797178&state=*

Finally gave it a better look today. It looks good. With this I should
be able to easily see how the unified range tracking differs from the
latest implementation once I have conditional jump logic implemented.
I've only got to add/sub/mul so far[2].

2: https://lore.kernel.org/bpf/20231108054611.19531-1-shung-hsi.yu@suse.com/

[...]

Re: Unifying signed and unsigned min/max tracking

[Shung-Hsi Yu]

On Fri, Oct 27, 2023 at 01:46:35PM -0700, Andrii Nakryiko wrote:
> On Thu, Oct 26, 2023 at 10:44 PM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
> > On Mon, Oct 23, 2023 at 09:14:08PM +0800, Shung-Hsi Yu 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).
> >
> > As per [1], PREVAIL uses the zone domain[2][3] to track values along with
> > relationships between values, where as the Linux Kernel tracks values with
> > min/max (i.e. interval domain) and tnum. In short, PREVAIL does not use this
> > trick, but I guess it probably don't need to since it's already using
> > something that considered to be more advanced.
> 
> tnum is actually critical for checking memory alignment (i.e.,
> checking that low 2-3 bits are always zero), which range tracking
> can't do. So I suspect PREVAIL doesn't validate those conditions,
> while kernel's verifier does.

I didn't know this :)

Looking into Wikipedia's article on Zone domain it seems that indeed it
cannot tell memory alignment.

> > Also, found some research papers on this topic referring to it as Wrapped
> > Intervals[4] or Modular Interval Domain[5]. The former has an MIT-licensed
> > C++ implementation[6] available as reference.
> >
> > 1: https://pchaigno.github.io/ebpf/2023/09/06/prevail-understanding-the-windows-ebpf-verifier.html
> > 2: https://en.wikipedia.org/wiki/Difference_bound_matrix#Zone
> > 3: https://github.com/vbpf/ebpf-verifier/blob/6d5ad53/src/crab/split_dbm.hpp
> > 4: https://dl.acm.org/doi/abs/10.1145/2651360
> 
> this one (judging by the name of the paper) looks exactly like what we
> are trying to do here. I'll give it a read some time later.

I'm putting off reading it fully (for some fun), and only went through
the introduction and a few figures so far. It does seem like it had
all the bits that I need to know to make this work.

Also, the use of circles to visualize the numerical domain in the paper
makes great intuitive sense, too bad my ASCII art skill is not good
enough to draw circles.

> ... Meanwhile
> I posted full patch set with range logic ([0]), feel free to take a
> look as well.
> 
>   [0] https://patchwork.kernel.org/project/netdevbpf/list/?series=797178&state=*

A bit late to the party, but I'm coming back to (the latest version of)
this series.

[...]