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

[Edward Cree <ecree@amd.com>]

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.

> It is worth noting that we can update the signed bounds using the unsigned
> bounds whenever the unsigned bounds do not cross the sign boundary (not
> just when the input signed bounds are positive, as was the case
> previously). This patch does exactly that
Commit message could also make clearer that the new code considers whether
 the *output* ubounds cross sign, rather than looking at the input bounds
 as the previous code did.  At first I was confused as to why XOR didn't
 need special handling (since -ve xor -ve is +ve).

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index fcb62300f407..a7404a7d690f 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -13326,23 +13326,21 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
>                 return;
>         }
> 
> -       /* We get our minimum from the var_off, since that's inherently
> +       /* We get our minimum from the var32_off, since that's inherently
>          * bitwise.  Our maximum is the minimum of the operands' maxima.
>          */

This change, adjusting a comment to match the existing code, should probably
 be in a separate patch.
> @@ -13395,23 +13391,21 @@ static void scalar32_min_max_or(struct bpf_reg_state *dst_reg,
>                 return;
>         }
> 
> -       /* We get our maximum from the var_off, and our minimum is the
> -        * maximum of the operands' minima
> +       /* We get our maximum from the var32_off, and our minimum is the
> +        * maximum of the operands' minima.
>          */

Same here.

Apart from that,
Acked-by: Edward Cree <ecree.xilinx@gmail.com>