[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <5e67e977eb4f_586d2b10f16785b8f5@john-XPS-13-9370.notmuch>
Date: Tue, 10 Mar 2020 12:24:39 -0700
From: John Fastabend <john.fastabend@...il.com>
To: Edward Cree <ecree@...arflare.com>,
Alexei Starovoitov <alexei.starovoitov@...il.com>,
John Fastabend <john.fastabend@...il.com>
Cc: yhs@...com, daniel@...earbox.net, netdev@...r.kernel.org,
bpf@...r.kernel.org
Subject: Re: [RFC PATCH 2/4] bpf: verifier, do explicit u32 bounds tracking
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
Powered by blists - more mailing lists