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

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2023-10-02 at 09:29 -0700, Alexei Starovoitov wrote:
[...]
> > I'd like to argue about B "widening" for a bit, as I think it might be
> > interesting in general, and put A aside for now. The algorithm for
> > widening looks as follows:
> > - In is_states_equal() for (sl->state.branches > 0 && is_iter_next_insn()) case:
> >   - Check if states are equal exactly:
> >     - ignore liveness marks on old state;
> >     - demand same type for registers and stack slots;
> >     - ignore precision marks, instead compare scalars using
> >       regs_exact() [this differs from my previous emails, I'm now sure
> >       that for this scheme to be correct regs_exact() is needed].
> >   - If there is an exact match then follow "hit" branch. The idea
> >     being that visiting exactly the same state can't produce new
> >     execution paths (like with graph traversal).
> 
> Right. Exactly the same C state won't produce new paths
> as seen in visited state V, but
> if C==V at the same insn indx it means we're in the infinite loop.

This is true in general, but for bpf_iter_next() we have a guarantee
that iteration would end eventually.

> > More formally, before pruning potential looping states we need to
> > make sure that all precision and read marks are in place.
> > To achieve this:
> > - Process states from env->head while those are available, in case if
> >   potential looping state (is_states_equal()) is reached put it to a
> >   separate queue.
> > - Once all env->head states are processed the only source for new read
> >   and precision marks is in postponed looping states, some of which
> >   might not be is_states_equal() anymore. Submit each such state for
> >   verification until fixed point is reached (repeating steps for
> >   env->head processing).
> 
> Comparing if (sl->state.branches) makes sense to find infinite loop.
> It's waste for the verifier to consider visited state V with branches > 0
> for pruning.
> The safety of V is unknown. The lack of liveness and precision
> is just one part. The verifier didn't conclude that V is safe yet.
> The current state C being equivalent to V doesn't tell us anything.
> 
> If infinite loop detection logic trips us, let's disable it.
> I feel the fix should be in process_iter_next_call() to somehow
> make it stop doing push_stack() when states_equal(N-1, N-2).

Consider that we get to the environment state where:
- all env->head states are exhausted;
- all potentially looping states (stored in as a separate set of
  states instead of env->head) are states_equal() to some already
  explored state.

I argue that if such environment state is reached the program should
be safe, because:
- Each looping state L is a sub-state of some explored state V and
  every path from V leads to either safe exit or another loop.
- Iterator loops are guaranteed to exit eventually.

Achieving this steady state is the mechanism that tells verifier that
there is no need to schedule exploration of the N+1 iteration level
for any iterator in the program.