On Thu, 2023-11-09 at 09:32 -0800, Andrii Nakryiko wrote:
> On Thu, Nov 9, 2023 at 7:20 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
> >
> > On Mon, 2023-10-30 at 22:03 -0700, Andrii Nakryiko wrote:
> > > > Given verifier checks actual value, r0 has to be precise, so we need to
> > > > propagate precision properly.
> > > >
> > > > Fixes: 69c087ba6225 ("bpf: Add bpf_for_each_map_elem() helper")
> > > > Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> >
> > I don't follow why this is necessary, could you please conjure
> > an example showing that current behavior is not safe?
> > This example could be used as a test case, as this change
> > seems to not be covered by test cases.
>
> We rely on callbacks to return specific value (0 or 1, for example),
> and use or might use that in kernel code. So if we rely on the
> specific value of a register, it has to be precise. Marking r0 as
> precise will have implications on other registers from which r0 was
> derived. This might have implications on state pruning and stuff. If
> r0 and its ancestors are not precise, we might erroneously assume some
> states are safe and prune them, even though they are not.
The r0 returned from bpf_loop's callback says bpf_loop to stop iteration,
bpf_loop returns the number of completed iterations. However, the return
value of bpf_loop modeled by verifier is unbounded scalar.
Same for map's for each.
I'm not sure we have callback calling functions that can expose this as a
safety issue.
[...]
