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

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2023-09-18 at 00:09 +0200, Kumar Kartikeya Dwivedi wrote:
[...]
> 
> I was planning to get to this eventually, but it's great if you are
> looking to do it.
> 
> > After some analysis I decided to go with Alexei's suggestion and
> > implement something similar to iterators for selected set of helper
> > functions that accept "looping" callbacks, such as:
> > - bpf_loop
> > - bpf_for_each_map_elem
> > - bpf_user_ringbuf_drain
> > - bpf_timer_set_callback (?)
> > 
> 
> The last one won't require this, I think. The callback only runs once,
> and asynchronously.
> Others you are missing are bpf_find_vma and the bpf_rbtree_add kfunc.
> While the latter is not an interator, it can invoke the same callback
> an unknown number of times.

Noted, thank you.

> The other major thing that needs to be checked is cases where callback
> will be executed zero times. There is some discussion on this in [0],
> where this bug was reported originally. Basically, we need to explore
> a path where the callback execution does not happen and ensure the
> program is still safe.
> 
> [0]: https://lore.kernel.org/bpf/CAP01T74cOJzo3xQcW6weURH+mYRQ7kAWMqQOgtd_ymSbhrOoMQ@mail.gmail.com
> 
> You could also consider taking the selftests from this link, some of
> them allow completely breaking safety properties of the verifier.

Thank you, I missed this thread.

[...]
> > I have a patch (at the end of this email) that correctly recognizes
> > the bpf_loop example in this thread as unsafe. However this patch has
> > a few deficiencies:
> > 
> > - verif_scale_strobemeta_bpf_loop selftest is not passing, because
> >   read_map_var function invoked from the callback continuously
> >   increments 'payload' pointer used in subsequent iterations.
> > 
> >   In order to handle such code I need to add an upper bound tracking
> >   for iteration depth (when such bound could be deduced).
> > 
> 
> Yes, either the loop converges before the upper limit is hit, or we
> keep unrolling it until we exhaust the deduced loop count passed to
> the bpf_loop helper. But we will need to mark the loop count argument
> register as precise when we make use of its value in such a case.

Yes, marking counter as precise makes sense but I think it would
happen automatically. My current plan is to mark index register as
bounded and use depth tracking only internally to decide whether to
schedule another "active" iteration state. If that would not be
sufficient, I will try assigning specific values for loop counter
(hesitate to do it to avoid conflict with convergence detection).

[...]
> > - the callback as bellow currently causes state explosion:
> > 
> >   static int precise1_callback(__u32 idx, struct precise1_ctx *ctx)
> >   {
> >       if (idx == 0)
> >           ctx->a = 1;
> >       if (idx == 1 && ctx->a == 1)
> >           ctx->b = 1;
> >       return 0;
> >   }
> > 
> >   I'm not sure yet what to do about this, there are several possibilities:
> >   - tweak the order in which states are visited (need to think about it);
> >   - check states in bpf_verifier_env::head (not explored yet) for
> >     equivalence and avoid enqueuing duplicate states.
> > 
> > 
> > I'll proceed addressing the issues above on Monday.
> > 
> 
> I think there is a class of programs that are nevertheless going to be
> broken now, as bpf_loop and others basically permitted incorrect code
> to pass through. And the iteration until we arrive at a fixpoint won't
> be able to cover all classes of loop bodies, so I think we will need
> to make a tradeoff in terms of expressibility vs verifier complexity.
> In general, cases like this with branches/conditional exit from the
> loop body which do not converge will lead to state explosion anyway.

This might be the case, however I found that specific issue with
"precise1_callback" could be resolved by using mark_force_checkpoint()
to mark iteration back-edges (same way it is done for regular iterators).
So maybe impact won't be that bad.

Thanks,
Eduard