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:27 -0700, Alexei Starovoitov wrote:
> On Fri, Jun 2, 2023 at 12:13 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Fri, 2023-06-02 at 11:50 -0700, Andrii Nakryiko wrote:
> > [...]
> > > > > The thread is long. Could you please describe it again in pseudo code?
> > > > 
> > > > - Add a function mark_precise_scalar_ids(struct bpf_verifier_env *env,
> > > >                                         struct bpf_verifier_state *st)
> > > >   such that it:
> > > >   - collect PRECISE_IDS: a set of IDs of all registers marked in env->bt
> > > >   - visit all registers with ids from PRECISE_IDS and make sure
> > > >     that these registers are marked in env->bt
> > > > - Call mark_precise_scalar_ids() from __mark_chain_precision()
> > > >   for each state 'st' visited by states chain processing loop,
> > > >   so that:
> > > >   - mark_precise_scalar_ids() is called for current state when
> > > >     __mark_chain_precision() is entered, reusing id assignments in
> > > >     current state;
> > > >   - mark_precise_scalar_ids() is called for each parent state, reusing
> > > >     id assignments valid at 'last_idx' instruction of that state.
> > > > 
> > > > The idea is that in situations like below:
> > > > 
> > > >    4: if (r6 > r7) goto +1
> > > >    5: r7 = r6
> > > >    --- checkpoint #1 ---
> > > >    6: <something>
> > > >    7: if (r7 > X) goto ...
> > > >    8: r7 = 0
> > > >    9: r9 += r6
> > > > 
> > > > The mark_precise_scalar_ids() would be called at:
> > > > - (9) and current id assignments would be used.
> > > > - (6) and id assignments saved in checkpoint #1 would be used.
> > > > 
> > > > If <something> is the code that modifies r6/r7 the link would be
> > > > broken and we would overestimate the set of precise registers.
> > > > 
> > > 
> > > To avoid this we need to recalculate these IDs on each new parent
> > > state, based on requested precision marks. If we keep a simple and
> > > small array of IDs and do a quick linear search over them for each
> > > SCALAR register, I suspect it should be very fast. I don't think in
> > > practice we'll have more than 1-2 IDs in that array, right?
> > 
> > I'm not sure I understand, could you please describe how it should
> > work for e.g.?:
> > 
> >     3: r6 &= 0xf            // assume safe bound
> >     4: if (r6 > r7) goto +1
> >     5: r7 = r6
> >     --- checkpoint #1 ---
> >     6: r7 = 0
> >     7: if (r7 > 10) goto exit;
> >     8: r7 = 0
> >     9: r9 += r6
> > 
> > __mark_chain_precision() would get to checkpoint #1 with only r6 as
> > precise, what should happen next?
> > 
> > As a side note: I added several optimizations:
> > - avoid allocation of scalar ids for constants;
> 
> +1
> 
> > - remove sole scalar ids from cached states;
> > - 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 :(

> 
> >     return false;
> > 
> > And I'm seeing almost zero performance overhead now.
> > So, maybe what we figured so far is good enough.
> > Need to add more tests, though.