On 3/30/24 5:35 PM, Harishankar Vishwanathan wrote:
On Sat, Mar 30, 2024 at 1:28 AM Andrii Nakryiko
<andrii.nakryiko@xxxxxxxxx> wrote:
On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
<harishankar.vishwanathan@xxxxxxxxx> wrote:
On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
On Thu, 2024-03-28 at 23:01 -0400, Harishankar Vishwanathan wrote:
[...]
@@ -13387,18 +13389,19 @@ static void scalar32_min_max_or(struct bpf_reg_state *dst_reg,
*/
dst_reg->u32_min_value = max(dst_reg->u32_min_value, umin_val);
dst_reg->u32_max_value = var32_off.value | var32_off.mask;
- if (dst_reg->s32_min_value < 0 || smin_val < 0) {
+ if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
Hello,
Could you please elaborate a bit, why do you use "> 0" not ">= 0" here?
It seems that having one of the min values as 0 shouldn't be an issue,
but maybe I miss something.
You are right, this is a mistake, I sent the wrong version of the patch. Thanks
for catching it. I will send a new patch.
Note that in the correct version i'll be sending, instead of the following
if condition,
if (dst_reg->s32_min_value >= 0 && smin_val >= 0 &&
(s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value)
it will use this if condition:
if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value)
Inside the if, the output signed bounds are updated using the unsigned
bounds; the only case in which this is unsafe is when the unsigned
bounds cross the sign boundary. The shortened if condition is enough to
prevent this. The shortened has the added benefit of being more
precise. We will make a note of this in the new commit message.
And that's exactly what reg_bounds_sync() checks as well, which is why
my question/suggestion to not duplicate this logic, rather reset s32
bounds to unknown (S32_MIN/S32_MAX), and let generic reg_bounds_sync()
handle the re-derivation of whatever can be derived.
We tried your suggestion (setting the bounds to be completely unbounded).
This would indeed make the abstract operator scalar(32)_min_max_and
sound. However, we found (through Agni and SMT verification) that our patch is
more precise than just unconditionally setting the signed bounds to unbounded
[S32_MIN/S32_MAX], [S64_MIN,S64_MAX].
For example, consider these inputs to BPF_AND:
dst_reg
-----------------------------------------
var_off.value: 8608032320201083347
var_off.mask: 615339716653692460
smin_value: 8070450532247928832
smax_value: 8070450532247928832
umin_value: 13206380674380886586
umax_value: 13206380674380886586
s32_min_value: -2110561598
s32_max_value: -133438816
u32_min_value: 4135055354
u32_max_value: 4135055354
src_reg
-----------------------------------------
var_off.value: 8584102546103074815
var_off.mask: 9862641527606476800
smin_value: 2920655011908158522
smax_value: 7495731535348625717
umin_value: 7001104867969363969
umax_value: 8584102543730304042
s32_min_value: -2097116671
s32_max_value: 71704632
u32_min_value: 1047457619
u32_max_value: 4268683090
After going through
tnum_and() -> scalar32_min_max_and() -> scalar_min_max_and() ->
reg_bounds_sync()
Our patch produces the following bounds for s32:
s32_min_value: -1263875629
s32_max_value: -159911942
Whereas, setting the signed bounds to unbounded in
scalar(32)_min_max_and produces:
s32_min_value: -1263875629
s32_max_value: -1
Our patch produces a tighter bound as you can see. We also confirmed
using SMT that
our patch always produces signed bounds that are equal to or more
precise than setting
the signed bounds to unbounded in scalar(32)_min_max_and.
Admittedly, this is a contrived example. It is likely the case that
such precision
gains are never realized in an actual BPF program.
Overall, both the fixes are sound. We're happy to send a patch for
either of them.
Given your version is more precise, then that would be preferred. Might
be good to have the above as part of the commit description for future
reference.
Thanks,
Daniel
