On Sun, Oct 1, 2023 at 6:40 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Fri, 2023-09-29 at 17:41 -0700, Alexei Starovoitov wrote:
> [...]
> > I suspect that neither option A "Exit or Loop" or B "widening"
> > are not correct.
> > In both cases we will do states_equal() with states that have
> > not reached exit and don't have live/precision marks.
>
> 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.
> - If there is no exact match but there is some state V which for
> which states_equal(V, C) and V and C differ only in inexact
> scalars:
> - copy C to state C';
> - mark range for above mentioned inexact scalars as unbound;
> - continue verification from C';
> - if C' verification fails discard it and resume verification from C.
>
> The hope here is that guess for "wide" scalars would be correct and
> range for those would not matter. In such case C' would be added to
> the explored states right after it's creation (as it is a checkpoint),
> and later verification would get to the explored C' copy again, so
> that exact comparison would prune further traversals.
>
> Unfortunately, this is riddled with a number of technical
> complications on implementation side.
> What Andrii suggests might be simpler.
>
> > The key aspect of the verifier state pruning is that safe states
> > in sl list explored all possible paths.
> > Say, there is an 'if' block after iter_destroy.
> > The push_stack/pop_stack logic is done as a stack to make sure
> > that the last 'if' has to be explored before earlier 'if' blocks are checked.
> > The existing bpf iter logic violated that.
> > To fix that we need to logically do:
> >
> > if (is_iter_next_insn(env, insn_idx))
> > if (states_equal(env, &sl->state, cur)) {
> > if (iter_state->iter.state == BPF_ITER_STATE_DRAINED)
> > goto hit;
> >
> > instead of BPF_ITER_STATE_ACTIVE.
> > In other words we need to process loop iter == 0 case first
> > all the way till bpf_exit (just like we do right now),
> > then process loop iter == 1 and let it exit the loop and
> > go till bpf_exit (hopefully state prune will find equal states
> > right after exit from the loop).
> > then process loop iter == 2 and so on.
> > If there was an 'if' pushed to stack during loop iter == 1
> > it has to be popped and explored all the way till bpf_exit.
> >
> > We cannot just replace BPF_ITER_STATE_ACTIVE with DRAINED.
> > It would still be ACTIVE with sl->state.branches==0 after that
> > state explored all paths to bpf_exit.
>
> This is similar to what Andrii suggests, please correct me if I'm wrong:
>
> > 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.
>
> 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).
