Re: [RFC PATCH 2/4] bpf: verifier, do explicit u32 bounds tracking

[John Fastabend <john.fastabend@gmail.com>]

Edward Cree wrote:
> On 09/03/2020 23:58, Alexei Starovoitov wrote:> Thinking about it differently... var_off is a bit representation of
> > 64-bit register. So that bit representation doesn't really have
> > 32 or 16-bit chunks. It's a full 64-bit register. I think all alu32
> > and jmp32 ops can update var_off without losing information.
> Agreed; AFAICT the 32-bit var_off should always just be the bottom
>  32 bits of the full var_off.

This seems to work.


> In fact, it seems like the only situations where 32-bit bounds are
>  needed are (a) the high and low halves of a 64-bit register are
>  being used separately, so e.g. r0 = (x << 32) | y with small known
>  bounds on y you want to track, or (b) 32-bit signed arithmetic.
> (a) doesn't seem like it's in scope to be supported, and (b) should
>  (I'm naïvely imagining) only need the s32 bounds, not the u32 or
>  var32.

I guess I'm not opposed to supporting (a) it seems like it should
be doable.

For (b) the primary reason is to keep symmetry between 32-bit and
64-bit cases. But also we could have mixed signed 32-bit comparisons
which this helps with.

Example tracking bounds with [x,y] being signed 32-bit
bounds and [x',y'] being unsigned 32-bit bounds.

    r1 = #                   [x,y],[x',y']
    w1 >    0 goto pc+y      [x,y],[1 ,y']
    w1 s> -10 goto pc+x      [-10,y],[1 ,y']

We can't really deduce much from that in __reg_deduce_bounds so
we get stuck with different bounds on signed and unsigned space.
Same case as 64-bit world fwiw. I guess we could do more work
and use 64-bit/32-bit together and deduce something but I find
this more work than its worth. Keeping separate signed/unsigned
makes things easy.

> 
> John Fastabend wrote:
> > For example, BPF_ADD will do a tnum_add() this is a different
> > operation when overflows happen compared to tnum32_add(). Simply
> > truncating tnum_add result to 32-bits is not the same operation.
> I don't see why.  Overflows from the low (tracked) 32 bits can only
>  affect the high 32.
>  Truncation should be a homomorphism from
>  Z_2^n to Z_2^m wrt. both addition and multiplication, and tnums
>  are just (a particular class of) subsets of those rings.

Agreed, no need for 32bit ops on tnums.

> Can you construct an example of a tnum addition that breaks the
>  homomorphism?

no, I'm convinced. There seems to be a proof that the above is
true if n>m.

> 
> -ed