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

[Eduard Zingerman <eddyz87@gmail.com>]

On Tue, 2023-09-26 at 09:25 -0700, Andrii Nakryiko wrote:
[...]
> > In other words there is a function states_equal' for comparison of
> > states when old{.branches > 0}, which differs from states_equal in
> > the following way:
> > - considers all registers read;
> > - considers all scalars precise.
> >
> 
> Not really. The important aspect is to mark registers that were
> required to be imprecise in old state as "required to be imprecise",
> and if later we decide that this register has to be precise, too bad,
> too late, game over (which is why I didn't propose it, this seems too
> restrictive).

Could you please elaborate a bit? What's wrong with the following:
Suppose I see a register R that differs between V and C an is not
precise in both. I fork C as C', mark R unbound in C' and proceed with
C' verification. At some point during that verification I see that
some precise R's value is necessary, thus C' verification fails.
If that happens verification resumes from C, otherwise C is discarded.
I also postpone read and precision marks propagation from C' to it's
parent until C' verification succeeds (if it succeeds).

[...]
> 1. If V and C (using your terminology from earlier, where V is the old
> parent state at some next() call instruction, and C is the current one
> on the same instruction) are different -- we just keep going. So
> always try to explore different input states for the loop.
> 
> 2. But if V and C are equivalent, it's too early to conclude anything.
> So enqueue C for later in a separate BFS queue (and perhaps that queue
> is per-instruction, actually; or maybe even per-state, not sure), and
> keep exploring all the other pending queues from the (global) DFS
> queue, until we get back to state V again. At that point we need to
> start looking at postponed states for that V state. But this time we
> should be sure that precision and read marks are propagated from all
> those terminatable code paths.
> 
> Basically, this tries to make sure that we do mark every register that
> is important for all the branching decision making, memory
> dereferences, etc. And just avoids going into endless loops with the
> same input conditions.
> 
> Give it some fresh thought and let's see if we are missing something
> again. Thanks!

This should work for examples we've seen so far.
Why do you think a separate per-instruction queue is necessary?
The way I read it the following algorithm should suffice:
- add a field bpf_verifier_env::iter_head similar to 'head' but for
  postponed looping states;
- add functions push_iter_stack(), pop_iter_stack() similar to
  push_stack() and pop_stack();
- modify is_state_visited() as follows:

 static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
 {
     ...
     while (sl) {
         ...
         if (sl->state.branches) {
             ...
             if (is_iter_next_insn(env, insn_idx)) {
                 if (states_equal(env, &sl->state, cur)) {
                     ...
                     iter_state = &func(env, iter_reg)->stack[spi].spilled_ptr;
                     if (iter_state->iter.state == BPF_ITER_STATE_ACTIVE) {
+                        // Don't want to proceed with 'cur' verification,
+                        // push it to iters queue to check again if states
+                        // are still equal after env->head is exahusted.
+                        if (env->stack_size != 0)
+                            push_iter_stack(env, cur, ...);
                         goto hit;
                     }
                 }
                 goto skip_inf_loop_check;
             }
     ...
 }
 
- modify do_check() to do pop_iter_stack() if pop_stack() is
  exhausted, the popped state would get into is_state_visited() and
  checked against old state, which at that moment should have all
  read/precision masks that env->head could have provided.

After working on "widening conjectures" implementation a bit this
approach seems to be much simpler. Need to think harder if I can break it.