Re: [PATCH v2 bpf-next] bpf: Fix latent unsoundness in and/or/xor value tracking

[Shung-Hsi Yu]

On Wed, Apr 03, 2024 at 10:40:23PM -0400, Harishankar Vishwanathan wrote:
> On Wed, Apr 3, 2024 at 9:25 AM Edward Cree <ecree@xxxxxxx> wrote:
> > On 4/2/24 22:20, Harishankar Vishwanathan wrote:
> > > Previous works [1, 2] have discovered and reported this issue. Our tool
> > > Agni [2, 3] consideres it a false positive. This is because, during the
> > > verification of the abstract operator scalar_min_max_and(), Agni restricts
> > > its inputs to those passing through reg_bounds_sync(). This mimics
> > > real-world verifier behavior, as reg_bounds_sync() is invariably executed
> > > at the tail of every abstract operator. Therefore, such behavior is
> > > unlikely in an actual verifier execution.
> > >
> > > However, it is still unsound for an abstract operator to set signed bounds
> > > such that smin_value > smax_value. This patch fixes it, making the abstract
> > > operator sound for all (well-formed) inputs.
> >
> > Just to check I'm understanding correctly: you're saying that the existing
> >  code has an undocumented precondition, that's currently maintained by the
> >  callers, and your patch removes the precondition in case a future patch
> >  (or cosmic rays?) makes a call without satisfying it?
> > Or is it in principle possible (just "unlikely") for a program to induce
> >  the current verifier to call scalar_min_max_foo() on a register that
> >  hasn't been through reg_bounds_sync()?
> > If the former, I think Fixes: is inappropriate here as there is no need to
> >  backport this change to stable kernels, although I agree the change is
> >  worth making in -next.
> 
> You are kind of right on both counts.
> 
> The existing code contains an undocumented precondition. When violated,
> scalar_min_max_and() can produce unsound s64 bounds (where smin > smax).
> Certain well-formed register state inputs can violate this precondition,
> resulting in eventual unsoundness. However, register states that have
> passed through reg_bounds_sync() -- or those that are completely known or
> completely unknown -- satisfy the precondition, preventing unsoundness.
> 
> Since we haven’t examined all possible paths through the verifier, and we
> cannot guarantee that every instruction preceding a BPF_AND in an eBPF
> program will maintain the precondition, we cannot definitively say that
> register state inputs to scalar_min_max_and() will always meet the
> precondition. There is a potential for an invocation of
> scalar_min_max_and() on a register state that hasn’t undergone
> reg_bounds_sync(). The patch indeed removes the precondition.
> 
> Given the above, please advise if we should backport this patch to older
> kernels (and whether I should use the fixes tag).

I suggested the fixes tag to Harishankar in the v1 patchset, admittedly
without a thorough understanding at the same level of above.

However, given smin_value > smax_value is something we check in
reg_bounds_sanity_check(), I would still vote to have the patch
backported to stable (with "Cc: stable@xxxxxxxxxxxxxxx"?) even if the
fixes tag is dropped. The overall change should be rather well contained
and isolated for relatively ease of backport; and probably save some
head scratching over the difference of behavior between mainline and
stable.

> [...]