Re: [PATCH bpf-next v2 1/4] bpf: verify scalar ids mapping in regsafe() using check_ids()

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2023-06-02 at 12:43 -0700, Alexei Starovoitov wrote:
> On Fri, Jun 2, 2023 at 12:37 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > > > - do a check as follows:
> > > >   if (rold->precise && rold->id && !check_ids(idmap, rold, rcur))
> > > 
> > > Ignoring rcur->id > 0 ? Is it safe?
> > 
> > Well, I thought about it a bit and arrived to the following reasoning:
> > - suppose checkpoint C exists, is proven safe and has
> >   registers r6=Pscalar(range1),id=0 and r7=Pscalar(range2),id=0
> > - this means that C is proven safe for any value of
> >   r6 in range1 and any value of r7 in range2
> > - having same id on r6 and r7 means that r6 and r7 share same value
> > - so this is just a special case of what's already proven.
> > 
> > But having written this down, it looks like I also need to verify
> > that range1 and range2 overlap :(
> 
> I'm lost.
> id==0 means there is no relationship between regs.
> with
> if (rold->precise && rold->id && !check_ids(idmap, rold, rcur))
> 
> and r6_old->precise
> we will only do range_within(rold, rcur) && tnum_in() check
> and will ignore r6_cur->id and its relationship with some other reg in cur.
> It could be ok.

Yes, but I just realized that for the following case:

  Old                      Cur
  r6=Pscalar(range1),id=0  r6=Pscalar(range1),id=1
  r7=Pscalar(range2),id=0  r7=Pscalar(range2),id=1

For 'Cur' to be a subset of 'Old' ranges range1 and range2
have to have non-empty overlap, so my new check:

  if (rold->precise && rold->id && !check_ids(idmap, rold, rcur))

is not fully correct.

It was a "clever" attempt to ignore solo scalar IDs in Cur without modifying Cur.
I'll think a bit more, sorry for a lot of noise.