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. > [...]
