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. 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. 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).
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.
> 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.
> 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.
> 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.
