Re: [BUG] verifier escape with iteration helpers (bpf_loop, ...)

[Eduard Zingerman <eddyz87@gmail.com>]

On Tue, 2023-10-03 at 19:57 -0700, Alexei Starovoitov wrote:
> > Yes. This may be an issue. I'll try to hack a layered variant I talked
> > before to see what are the underlying issues. The idea is to verify
> > every child state of the loop entry before moving to any branches of
> > loop's parent states. 
> 
> Isn't that what current DFS logic does?

With a twist: it should wait for local loop convergence before
declaring loop entry state safe. I described it in [1].
Upon entry to a top level loop state E:
1. do DFS for E, disallow switching to any branches that are not
   children of E, collect all loop states generated by E's DFS;
3. reschedule loop states;
4. do DFS for rescheduled states, collect all loop states generated in
   the process;
5. repeat from 3 until no loop state could be rescheduled;
6. mark E safe, proceed from regular states stack.

[1] https://lore.kernel.org/bpf/8b75e01d27696cd6661890e49bdc06b1e96092c7.camel@gmail.com/

> > The idea is that when `env->stack.size == 0` all V's non-delayed
> > children states are explored and relevant precision marks are
> > propagated to V. 
> 
> But that is not true.
> if (is_iter_next_insn(env, insn_idx)) {
>   if (states_equal(env, &sl->state, cur)) {
> with sl->state.branches > 0
> will prevent exploration of all children.

Yes, it would postpone exploration of some children, but it would be
given a chance to reschedule.

> Hence I still believe that fine tunning this equavalence check is
> the first step in any fix.

Maybe, but so far states_equal(V, C) seems ok:
1. values read by V are defined in C;
2. non-precise scalars are equivalent unconditionally;
3. precise scalars in C are sub-ranges of precise scalars in V;
4. non-scalar values are compared exactly (modulo idmap).

Which of these points are overly optimistic in your opinion?

> > If at this point some states_equal(V, C') is false it
> > is necessary to schedule C' for one more exploration round as it might
> > visit some code blocks that were not visited on the path from V to C'
> > (as different predictions decisions could be made).
> 
> exactly my point above,
> but because of broken double 'if' above the 2nd pass might be hitting
> the same issues as the first. Because some path wasn't explored
> the precision marks might still be wrong.
> 
> More loop states can be created and delayed again into loop_stack?

Yes, and new reschedule would be done and so on.

> > If a point is reached when for all loop states C' there are some
> > states V such that states_equal(V, C'), there are no more
> > configurations that can visit code blocks not visited on the path from
> > V to C', as prediction decisions would be the same.
> 
> and it not, we can repeat loop_stack->stack->loop_stack potentially forever?

It might be the case that such logic would not converge, e.g. as in
the following simple example:

  it = iter_new();
  i = 0;
  while (iter_next(it)) {
    if (i & 0x1 == 0)
      printk("'i' is precise and different in each state");
    ++i;
  }
  iter_destroy(it);

However:
- we have such limitation already;
- examples like this don't play well with current states pruning logic
  in general (I think that doing some opportunistic widening of
  precise values is an interesting idea (loosing or worsening precision
  with ability to backtrack on failure), but this is a different topic).

If loop logic would not converge verifier would report an error:
either instruction or jump limit would be reached.

For the cases when this logic does converge we end up in a state when
no new read or precision marks could be gained, thus it is safe to
accept states_equal == true verdicts.

> Did you look at my broken patch? yes. it's buggy, but it demonstrates
> the idea where it removes above problematic double 'if' and uses
> states_equal() on states where st->branches==0 && st->looping_states==1

<replied in a different email>

> meaning that in those states all paths were explored except the one
> forked by iter_next kfunc.
> So precision and liveness is correct,

That's probably true.

> while doing states_equal on V with branches=2+ is broken.

Not that it is broken, but it's meaning is "maybe a sub-state" instead
of "definitely a sub-state".