On Mon, 2023-10-02 at 17:05 -0700, Alexei Starovoitov wrote:
[...]
> > 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.
>
> It sounds correct, but I don't like that the new mechanism
> with two stacks of states completely changes the way the verifier works.
> The check you proposed:
> if (env->stack_size != 0)
> push_iter_stack()
> rings alarm bells.
>
> env->stack_size == 0 (same as env->head exhausted) means we're done
> with verification (ignoring bpf_exit in callbacks and subprogs).
> So above check looks like a hack for something that I don't understand yet.
> Also there could be branches in the code before and after iter loop.
> With "opportunistic" states_equal() for looping states and delayed
> reschedule_loop_states() to throw states back at the verifier
> the whole verification model is non comprehensible (at least to me).
> The stack + iter_stack + reschedule_loop_states means that in the following:
> foo()
> {
> br1 // some if() {...} block
> loop {
> br2
> }
> br3
> }
>
> the normal verifier pop_stack logic will check br3 and br1,
> but br2 may or may not be checked depending on "luck" of states_equal
> and looping states that will be in iter_stack.
> Then the verifier will restart from checking loop-ing states.
>
> If they somehow go past the end of the loop all kinds of things go crazy.
> update_branch_counts() might warn, propagate_liveness, propagate_precision
> will do nonsensical things.
When I put states to the loop stack I do copy_verifier_state() and
increase .branches counter for each state parent, so this should not
trigger warnings with update_branch_counts(). Logically, any state
that has a loop state as it's grandchild is not verified to be safe
until loops steady state is achieved, thus such states could not be
used for states pruning and it is correct to keep their branch
counters > 0.
propagate_liveness() and propagate_precision() should not be called
for the delayed states (work-in-progress I'll update the patch).
Behavior for non-delayed states should not be altered by these changes.
> This out-of-order state processing distorts the existing model so
> much that I don't see how we can reason about these two stacks verification.
Iterators (and callbacks) try to diverge from regular verification
logic of visiting all possible paths by making some general
assumptions about loop bodies. There is no way to verify safety of
such bodies w/o computing steady states.
> I think the cleaner solution is to keep current single stack model.
> In the above example the verifier would reach the end, then check br3,
> then check br2,
> then we need to split branches counter somehow, so that we can
> compare loop iter states with previous visited states that are known
> to be safe.
> In visited states we explored everything in br3 and in br2,
> so no concerns that some path inside the loop or after the loop
> missed precision or liveness.
>
> Maybe we can split branches counter into branches due to 'if' blocks
> and branches due to process_iter_next_call().
> If there are pending process_iter_next_call-caused states it's still
> ok to call states_equal on such visited states.
Using a stack forces DFS states traversal, if there is a loop state
with branching this is prone to infinite nesting, e.g.:
0. // Complete assembly code is in the end of the email.
1. while (next(i)) {
2. if (random())
3. continue;
4. r0 += 0;
5. }
Would lead to an infinite loop when using the patch shared in [1].
At (2) verifier would always create a state with {.loop_state=false},
thus checkpoint state at (1) would always have
`sl->branches != sl->state.looping_states`:
- looping state is current one,
- non-looping state is the "else" branch scheduled in (2).
Therefore checkpoint in (1) is not eligible for pruning and verifier
would eagerly descend via path 1,2,3,1,2,3,...
I don't think this is a quirk of the patch, with only a single stack
there are no means to postpone exploration.
Note, that removal of `elem->st.looping_state = false;` from
push_stack() is not safe either, precision marks and unsafe values
could be concealed in nested iteration states as shown in example [2],
so we are risking pruning some states too early.
[1] https://lore.kernel.org/bpf/CAADnVQJ3=x8hfv7d29FQ-ckzh9=MXo54cnFShFp=eG0fJjdDow@xxxxxxxxxxxxxx/T/#m8fc0fc3e338f57845f9fb65e0c3798a2ef5fb2e7
[2] https://lore.kernel.org/bpf/CAADnVQJ3=x8hfv7d29FQ-ckzh9=MXo54cnFShFp=eG0fJjdDow@xxxxxxxxxxxxxx/T/#m6014e44a00ab7732890c13b83b5497f8d856fc81
---
In theory, loops steady state does not have to be tracked globally it
can be tracked per some key states, e.g. entry states for top-level loops:
- at the entry state E for a top level loop:
- establish a separate regular and loop state stacks: E.stack, E.loop_stack;
- add E to explored states as a checkpoint and continue verification
from E' a copy of E (at this point E branches counter is > 0);
- in is_state_visited() / .branches > 0 / is_bpf_next_insn():
- only consider current state C for states_equal(V, C) if V and C
have a common grandparent E;
- use E.loop_stack to delay C;
- use same logic for steady state as before:
- E.stack should be exhausted;
- states in E.loop_stack should all be states_equal() to some
explored state V that has E as it's grandparent.
- if such steady state is achieved E's loop states could be dropped
and branches counter for E could be set to 0, thus opening it up for
regular states pruning.
Such logic would make verification of loops more similar to
verification of regular conditionals, e.g.:
foo() {
if (random()) {
r0 = 0; // branch B1
} else {
r0 = 42; // branch B2
}
i = iter_new();
// loop entry E
while (iter_next()) {
// loop body LB
do_something();
}
}
Here verifier would first visit path B1,E,LB, second visit to LB would
be delayed and steady state for E would be declared, E.branches would
be set to 0. Then path B1,E would be visited and declared safe as E is
eligible for states pruning.
This gives more opportunities for states pruning and makes user's
reasoning about iterators verification similar to user's reasoning
about regular loops verification.
But it adds some more complexity to the implementation
(albeit, I think it's not much, env->head becomes a stack of stacks
and a few other tweaks).
---
SEC("?raw_tp")
__success
__naked int loop1(void)
{
asm volatile (
"r1 = r10;"
"r1 += -8;"
"r2 = 0;"
"r3 = 10;"
"call %[bpf_iter_num_new];"
"loop_%=:"
"r1 = r10;"
"r1 += -8;"
"call %[bpf_iter_num_next];"
"if r0 == 0 goto loop_end_%=;"
"call %[bpf_get_prandom_u32];"
"if r0 != 42 goto loop_%=;"
"r0 += 0;"
"goto loop_%=;"
"loop_end_%=:"
"r1 = r10;"
"r1 += -8;"
"call %[bpf_iter_num_destroy];"
"r0 = 0;"
"exit;"
:
: __imm(bpf_get_prandom_u32),
__imm(bpf_iter_num_new),
__imm(bpf_iter_num_next),
__imm(bpf_iter_num_destroy)
: __clobber_all
);
}
