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@xxxxxxxxx>
