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). > > 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). Sounds good regarding making it clearer within the context of what the existing code does. However, I wanted to clarify that XOR does indeed use the same handling as all the other operations. Could you elaborate on what you mean? > > 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. Sounds good. > > @@ -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>
