On Wed, Oct 04, 2023 at 04:05:30AM +0300, Eduard Zingerman wrote:
> On Tue, 2023-10-03 at 16:08 -0700, Alexei Starovoitov wrote:
> [...]
> > > When bpf_iter_next() is reached in state C and states_equal() shows
> > > that there is potentially equivalent state V:
> > > - copy C' of C is created sing copy_verifier_state(), it updates all
> > > branch counters up the ownership chain as with any other state;
> > > - C' is put to env->loop_stack.
> >
> > and C' points to normal parent and increments its branches as part of __push_stack().
>
> Yes.
>
> > void foo()
> > {
> > if (...) { .. } // no pruning
> > if (...) { .. } // no pruning
> >
> > bpf_for(...)
> > if (...) { .. } // all ok
> > }
> >
> > Essentially any complex code before the loop has a high chance of the verifier
> > state explosion.
>
> 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?
> This would allow to compute local "steady loop"
> and mark everything after loop entry as safe (.branches == 0).
>
> > > It is possible and correct to propagate liveness and precision from V
> > > to C when loop steady state is achieved, as at that point we know for
> > > sure that C is a sub-state of V. However, currently loop states are
> > > tracked globally and no states are processed after loops steady state
> > > is reached, hence I don't do liveness and precision propagation.
> >
> > Hmm. I think the code is doing it:
> > if (is_iter_next_insn(env, insn_idx)) {
> > if (states_equal(env, &sl->state, cur)) {
> > push_loop_stack(env, insn_idx, env->prev_insn_idx);
> > goto hit;
> > hit:
> > propagate_liveness()
>
> Yes and this should be changed. It should not produce incorrect
> results as additional precision and read marks are conservative,
> but will hinder state pruning in some scenarios.
>
> > DFS + BFS traversal doesn't guarantee safety.
> > We delayed looping states in loop_stack, but it doesn't mean
> > that the loop body reached a steady state.
> > Your own num_iter_bug() is an example.
> > The verifier will miss exploring path with r7 = 0xdead.
> > When C' is popped from loop_stack there is chance it will explore them,
> > but there is no guarantee.
> > For this particular num_iter_bug() case the loop processing
> > will eventually propagate precision marks and retrying with C' later,
> > the C' will be correctly rejected, since precision marks are there.
> > But I think that is more due to luck and the shape of the test.
> >
> > if (is_iter_next_insn(env, insn_idx)) {
> > if (states_equal(env, &sl->state, cur)) {
> >
> > is a foot gun. It finds broken equivalence and potentially skipping
> > whole blocks of code.
> > What guarantees that C' from loop_stack will explore them?
>
> 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.
Hence I still believe that fine tunning this equavalence check is
the first step in any fix.
> 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?
> 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?
> > I think avoiding states_equal(V, cur) when V state didn't converge
> > is a mandatory part of the fix.
>
> But there are no other heuristics that suggest that exploration of the
> infinite series of loop iterations could be stopped for current path.
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
meaning that in those states all paths were explored except the one
forked by iter_next kfunc.
So precision and liveness is correct,
while doing states_equal on V with branches=2+ is broken. It's a guess.
Could just be random true/false and algorithm of delaying looping states
will probably converge the same way on the tests we have so far.
> > I can see that little bit of out-of-order state processing probably
> > is still correct, but delaying loop_stack all the way until
> > env->stack.size == 0 is just broken.
> > For example we can push looping state in process_iter_next_call()
> > not the top of the stack, but place it after branches with
> > insn_idx >= iter_next's insn_idx.
>
> This should be based on state parentage chain as code blocks could be
> non-linearly structured.
ok. discard that idea.
> > This way the delayed looping states will still be processed
> > around loop processing and every code block before the loop
> > will converge to branches = 0.
> > To do that we don't need another loop_stack.
>
> Will comment in the morning.
