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

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

[Harishankar Vishwanathan]

The scalar(32)_min_max_and/or/xor functions can exhibit unsound behavior
when setting signed bounds. The following example illustrates the issue for
scalar_min_max_and(), but it applies to the other functions.

In scalar_min_max_and() the following clause is executed when ANDing
positive numbers:

		/* ANDing two positives gives a positive, so safe to
		 * cast result into s64.
		 */
		dst_reg->smin_value = dst_reg->umin_value;
		dst_reg->smax_value = dst_reg->umax_value;

However, if umin_value and umax_value of dst_reg cross the sign boundary
(i.e., if (s64)dst_reg->umin_value > (s64)dst_reg->umax_value), then we
will end up with smin_value > smax_value, which is unsound.

Previous works [1, 2] have discovered and reported this issue. Our tool
Agni [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 exhibit behavior
where smin_value > smax_value. This patch fixes it, making the abstract
operator sound for all (well-formed) inputs.

It's worth noting that this patch only modifies the output signed bounds
(smin/smax_value) in cases where it was previously unsound. As such, there
is no change in precision. When the unsigned bounds (umin/umax_value) cross
the sign boundary, they shouldn't be used to update  the signed bounds
(smin/max_value). In only such cases, we set the output signed bounds to
unbounded [S64_MIN, S64_MAX]. We confirmed through SMT verification that
the problem occurs if and only if the unsigned bounds cross the sign
boundary.

[1] https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf
[2] https://github.com/bpfverif/agni
[3] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_12

Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
---
 kernel/bpf/verifier.c | 76 +++++++++++++++++++++++--------------------
 1 file changed, 40 insertions(+), 36 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index ca6cacf7b42f..9bc4c2b1ca2e 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -13318,18 +13318,19 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
 	 */
 	dst_reg->u32_min_value = var32_off.value;
 	dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val);
-	if (dst_reg->s32_min_value < 0 || smin_val < 0) {
+	if (dst_reg->s32_min_value >= 0 && smin_val >= 0 &&
+		(s32)dst_reg->u32_min_value < (s32)dst_reg->u32_max_value) {
+		/* ANDing two positives gives a positive, so safe to cast
+		 * u32 result into s32 when u32 doesn't cross sign boundary.
+		 */
+		dst_reg->s32_min_value = dst_reg->u32_min_value;
+		dst_reg->s32_max_value = dst_reg->u32_max_value;
+	} else {
 		/* Lose signed bounds when ANDing negative numbers,
 		 * ain't nobody got time for that.
 		 */
 		dst_reg->s32_min_value = S32_MIN;
 		dst_reg->s32_max_value = S32_MAX;
-	} else {
-		/* ANDing two positives gives a positive, so safe to
-		 * cast result into s64.
-		 */
-		dst_reg->s32_min_value = dst_reg->u32_min_value;
-		dst_reg->s32_max_value = dst_reg->u32_max_value;
 	}
 }
 
@@ -13351,18 +13352,19 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg,
 	 */
 	dst_reg->umin_value = dst_reg->var_off.value;
 	dst_reg->umax_value = min(dst_reg->umax_value, umax_val);
-	if (dst_reg->smin_value < 0 || smin_val < 0) {
+	if (dst_reg->smin_value >= 0 && smin_val >= 0 &&
+		(s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
+		/* ANDing two positives gives a positive, so safe to cast
+		 * u64 result into s64, when u64 doesn't cross sign boundary.
+		 */
+		dst_reg->smin_value = dst_reg->umin_value;
+		dst_reg->smax_value = dst_reg->umax_value;
+	} else {
 		/* Lose signed bounds when ANDing negative numbers,
 		 * ain't nobody got time for that.
 		 */
 		dst_reg->smin_value = S64_MIN;
 		dst_reg->smax_value = S64_MAX;
-	} else {
-		/* ANDing two positives gives a positive, so safe to
-		 * cast result into s64.
-		 */
-		dst_reg->smin_value = dst_reg->umin_value;
-		dst_reg->smax_value = dst_reg->umax_value;
 	}
 	/* We may learn something more from the var_off */
 	__update_reg_bounds(dst_reg);
@@ -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 &&
+		(s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
+		/* ORing two positives gives a positive, so safe to cast
+		 * u32 result into s32 when u32 doesn't cross sign boundary.
+		 */
+		dst_reg->s32_min_value = dst_reg->u32_min_value;
+		dst_reg->s32_max_value = dst_reg->u32_max_value;
+	} else {
 		/* Lose signed bounds when ORing negative numbers,
 		 * ain't nobody got time for that.
 		 */
 		dst_reg->s32_min_value = S32_MIN;
 		dst_reg->s32_max_value = S32_MAX;
-	} else {
-		/* ORing two positives gives a positive, so safe to
-		 * cast result into s64.
-		 */
-		dst_reg->s32_min_value = dst_reg->u32_min_value;
-		dst_reg->s32_max_value = dst_reg->u32_max_value;
 	}
 }
 
@@ -13420,18 +13423,19 @@ static void scalar_min_max_or(struct bpf_reg_state *dst_reg,
 	 */
 	dst_reg->umin_value = max(dst_reg->umin_value, umin_val);
 	dst_reg->umax_value = dst_reg->var_off.value | dst_reg->var_off.mask;
-	if (dst_reg->smin_value < 0 || smin_val < 0) {
+	if (dst_reg->smin_value >= 0 && smin_val >= 0 &&
+		(s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
+		/* ORing two positives gives a positive, so safe to cast
+		 * u64 result into s64 when u64 doesn't cross sign boundary.
+		 */
+		dst_reg->smin_value = dst_reg->umin_value;
+		dst_reg->smax_value = dst_reg->umax_value;
+	} else {
 		/* Lose signed bounds when ORing negative numbers,
 		 * ain't nobody got time for that.
 		 */
 		dst_reg->smin_value = S64_MIN;
 		dst_reg->smax_value = S64_MAX;
-	} else {
-		/* ORing two positives gives a positive, so safe to
-		 * cast result into s64.
-		 */
-		dst_reg->smin_value = dst_reg->umin_value;
-		dst_reg->smax_value = dst_reg->umax_value;
 	}
 	/* We may learn something more from the var_off */
 	__update_reg_bounds(dst_reg);
@@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
 	/* We get both minimum and maximum from the var32_off. */
 	dst_reg->u32_min_value = var32_off.value;
 	dst_reg->u32_max_value = var32_off.value | var32_off.mask;
-
-	if (dst_reg->s32_min_value >= 0 && smin_val >= 0) {
-		/* XORing two positive sign numbers gives a positive,
-		 * so safe to cast u32 result into s32.
+	if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
+		(s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
+		/* XORing two positives gives a positive, so safe to cast
+		 * u32 result into s32 when u32 doesn't cross sign boundary.
 		 */
 		dst_reg->s32_min_value = dst_reg->u32_min_value;
 		dst_reg->s32_max_value = dst_reg->u32_max_value;
@@ -13482,10 +13486,10 @@ static void scalar_min_max_xor(struct bpf_reg_state *dst_reg,
 	/* We get both minimum and maximum from the var_off. */
 	dst_reg->umin_value = dst_reg->var_off.value;
 	dst_reg->umax_value = dst_reg->var_off.value | dst_reg->var_off.mask;
-
-	if (dst_reg->smin_value >= 0 && smin_val >= 0) {
-		/* XORing two positive sign numbers gives a positive,
-		 * so safe to cast u64 result into s64.
+	if (dst_reg->smin_value >= 0 && smin_val >= 0 &&
+		(s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
+		/* XORing two positives gives a positive, so safe to cast
+		 * u64 result into s64 when u64 doesn't cross sign boundary.
 		 */
 		dst_reg->smin_value = dst_reg->umin_value;
 		dst_reg->smax_value = dst_reg->umax_value;
-- 
2.40.1

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

[Shung-Hsi Yu]

On Thu, Mar 28, 2024 at 11:01:19PM -0400, Harishankar Vishwanathan wrote:
> The scalar(32)_min_max_and/or/xor functions can exhibit unsound behavior
> when setting signed bounds. The following example illustrates the issue for
> scalar_min_max_and(), but it applies to the other functions.
> 
> In scalar_min_max_and() the following clause is executed when ANDing
> positive numbers:
> 
> 		/* ANDing two positives gives a positive, so safe to
> 		 * cast result into s64.
> 		 */
> 		dst_reg->smin_value = dst_reg->umin_value;
> 		dst_reg->smax_value = dst_reg->umax_value;
> 
> However, if umin_value and umax_value of dst_reg cross the sign boundary
> (i.e., if (s64)dst_reg->umin_value > (s64)dst_reg->umax_value), then we
> will end up with smin_value > smax_value, which is unsound.
> 
> Previous works [1, 2] have discovered and reported this issue. Our tool
> Agni [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 exhibit behavior
> where smin_value > smax_value. This patch fixes it, making the abstract
> operator sound for all (well-formed) inputs.
> 
> It's worth noting that this patch only modifies the output signed bounds
> (smin/smax_value) in cases where it was previously unsound. As such, there
> is no change in precision. When the unsigned bounds (umin/umax_value) cross
> the sign boundary, they shouldn't be used to update  the signed bounds
> (smin/max_value). In only such cases, we set the output signed bounds to
> unbounded [S64_MIN, S64_MAX]. We confirmed through SMT verification that
> the problem occurs if and only if the unsigned bounds cross the sign
> boundary.
> 
> [1] https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf
> [2] https://github.com/bpfverif/agni
> [3] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_12
> 
> Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>

I'd suggest adding a fixes tag as well. This seems to go all the way
back to the signed/unsigned split.

Fixed: b03c9f9fdc37 ("bpf/verifier: track signed and unsigned min/max values")

Otherwise

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

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

[Shung-Hsi Yu]

On Fri, Mar 29, 2024 at 02:34:00PM +0800, Shung-Hsi Yu wrote:
> [...]
> Fixed: b03c9f9fdc37 ("bpf/verifier: track signed and unsigned min/max values")

Should have been

Fixes: b03c9f9fdc37 ("bpf/verifier: track signed and unsigned min/max values")

Sorry for the noise.

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

[Eduard Zingerman]

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.

> +		(s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> +		/* ORing two positives gives a positive, so safe to cast
> +		 * u32 result into s32 when u32 doesn't cross sign boundary.
> +		 */
> +		dst_reg->s32_min_value = dst_reg->u32_min_value;
> +		dst_reg->s32_max_value = dst_reg->u32_max_value;
> +	} else {
>  		/* Lose signed bounds when ORing negative numbers,
>  		 * ain't nobody got time for that.
>  		 */
>  		dst_reg->s32_min_value = S32_MIN;
>  		dst_reg->s32_max_value = S32_MAX;
> -	} else {
> -		/* ORing two positives gives a positive, so safe to
> -		 * cast result into s64.
> -		 */
> -		dst_reg->s32_min_value = dst_reg->u32_min_value;
> -		dst_reg->s32_max_value = dst_reg->u32_max_value;
>  	}
>  }

[...]

> @@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
>  	/* We get both minimum and maximum from the var32_off. */
>  	dst_reg->u32_min_value = var32_off.value;
>  	dst_reg->u32_max_value = var32_off.value | var32_off.mask;
> -
> -	if (dst_reg->s32_min_value >= 0 && smin_val >= 0) {
> -		/* XORing two positive sign numbers gives a positive,
> -		 * so safe to cast u32 result into s32.
> +	if (dst_reg->s32_min_value > 0 && smin_val > 0 &&

Same question here.

> +		(s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> +		/* XORing two positives gives a positive, so safe to cast
> +		 * u32 result into s32 when u32 doesn't cross sign boundary.
>  		 */
>  		dst_reg->s32_min_value = dst_reg->u32_min_value;
>  		dst_reg->s32_max_value = dst_reg->u32_max_value;

[...]

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

[Andrii Nakryiko]

On Thu, Mar 28, 2024 at 8:02 PM Harishankar Vishwanathan
<harishankar.vishwanathan@gmail.com> wrote:
>
> The scalar(32)_min_max_and/or/xor functions can exhibit unsound behavior
> when setting signed bounds. The following example illustrates the issue for
> scalar_min_max_and(), but it applies to the other functions.
>
> In scalar_min_max_and() the following clause is executed when ANDing
> positive numbers:
>
>                 /* ANDing two positives gives a positive, so safe to
>                  * cast result into s64.
>                  */
>                 dst_reg->smin_value = dst_reg->umin_value;
>                 dst_reg->smax_value = dst_reg->umax_value;
>
> However, if umin_value and umax_value of dst_reg cross the sign boundary
> (i.e., if (s64)dst_reg->umin_value > (s64)dst_reg->umax_value), then we
> will end up with smin_value > smax_value, which is unsound.
>
> Previous works [1, 2] have discovered and reported this issue. Our tool
> Agni [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 exhibit behavior
> where smin_value > smax_value. This patch fixes it, making the abstract
> operator sound for all (well-formed) inputs.
>
> It's worth noting that this patch only modifies the output signed bounds
> (smin/smax_value) in cases where it was previously unsound. As such, there
> is no change in precision. When the unsigned bounds (umin/umax_value) cross
> the sign boundary, they shouldn't be used to update  the signed bounds
> (smin/max_value). In only such cases, we set the output signed bounds to
> unbounded [S64_MIN, S64_MAX]. We confirmed through SMT verification that
> the problem occurs if and only if the unsigned bounds cross the sign
> boundary.
>
> [1] https://sanjit-bhat.github.io/assets/pdf/ebpf-verifier-range-analysis22.pdf
> [2] https://github.com/bpfverif/agni
> [3] https://link.springer.com/chapter/10.1007/978-3-031-37709-9_12
>
> Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> ---
>  kernel/bpf/verifier.c | 76 +++++++++++++++++++++++--------------------
>  1 file changed, 40 insertions(+), 36 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index ca6cacf7b42f..9bc4c2b1ca2e 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -13318,18 +13318,19 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
>          */
>         dst_reg->u32_min_value = var32_off.value;
>         dst_reg->u32_max_value = min(dst_reg->u32_max_value, umax_val);
> -       if (dst_reg->s32_min_value < 0 || smin_val < 0) {
> +       if (dst_reg->s32_min_value >= 0 && smin_val >= 0 &&
> +               (s32)dst_reg->u32_min_value < (s32)dst_reg->u32_max_value) {
> +               /* ANDing two positives gives a positive, so safe to cast
> +                * u32 result into s32 when u32 doesn't cross sign boundary.
> +                */
> +               dst_reg->s32_min_value = dst_reg->u32_min_value;
> +               dst_reg->s32_max_value = dst_reg->u32_max_value;
> +       } else {
>                 /* Lose signed bounds when ANDing negative numbers,
>                  * ain't nobody got time for that.
>                  */
>                 dst_reg->s32_min_value = S32_MIN;
>                 dst_reg->s32_max_value = S32_MAX;
> -       } else {
> -               /* ANDing two positives gives a positive, so safe to
> -                * cast result into s64.
> -                */
> -               dst_reg->s32_min_value = dst_reg->u32_min_value;
> -               dst_reg->s32_max_value = dst_reg->u32_max_value;
>         }

have you tried just unconditionally setting s32_{min,max}_value to
S32_{MIN,MAX} and letting reg_bounds_sync perform u32/s32 bounds
derivation?

>  }
>

[...]

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

[Harishankar Vishwanathan]

On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@gmail.com> 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.

This applies to all scalar(32)_min_max_and/or/xor.

> > +             (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > +             /* ORing two positives gives a positive, so safe to cast
> > +              * u32 result into s32 when u32 doesn't cross sign boundary.
> > +              */
> > +             dst_reg->s32_min_value = dst_reg->u32_min_value;
> > +             dst_reg->s32_max_value = dst_reg->u32_max_value;
> > +     } else {
> >               /* Lose signed bounds when ORing negative numbers,
> >                * ain't nobody got time for that.
> >                */
> >               dst_reg->s32_min_value = S32_MIN;
> >               dst_reg->s32_max_value = S32_MAX;
> > -     } else {
> > -             /* ORing two positives gives a positive, so safe to
> > -              * cast result into s64.
> > -              */
> > -             dst_reg->s32_min_value = dst_reg->u32_min_value;
> > -             dst_reg->s32_max_value = dst_reg->u32_max_value;
> >       }
> >  }
>
> [...]
>
> > @@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
> >       /* We get both minimum and maximum from the var32_off. */
> >       dst_reg->u32_min_value = var32_off.value;
> >       dst_reg->u32_max_value = var32_off.value | var32_off.mask;
> > -
> > -     if (dst_reg->s32_min_value >= 0 && smin_val >= 0) {
> > -             /* XORing two positive sign numbers gives a positive,
> > -              * so safe to cast u32 result into s32.
> > +     if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
>
> Same question here.
>
> > +             (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > +             /* XORing two positives gives a positive, so safe to cast
> > +              * u32 result into s32 when u32 doesn't cross sign boundary.
> >                */
> >               dst_reg->s32_min_value = dst_reg->u32_min_value;
> >               dst_reg->s32_max_value = dst_reg->u32_max_value;
>
> [...]

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

[Andrii Nakryiko]

On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
<harishankar.vishwanathan@gmail.com> wrote:
>
> On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@gmail.com> 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.

>
> This applies to all scalar(32)_min_max_and/or/xor.
>
> > > +             (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > > +             /* ORing two positives gives a positive, so safe to cast
> > > +              * u32 result into s32 when u32 doesn't cross sign boundary.
> > > +              */
> > > +             dst_reg->s32_min_value = dst_reg->u32_min_value;
> > > +             dst_reg->s32_max_value = dst_reg->u32_max_value;
> > > +     } else {
> > >               /* Lose signed bounds when ORing negative numbers,
> > >                * ain't nobody got time for that.
> > >                */
> > >               dst_reg->s32_min_value = S32_MIN;
> > >               dst_reg->s32_max_value = S32_MAX;
> > > -     } else {
> > > -             /* ORing two positives gives a positive, so safe to
> > > -              * cast result into s64.
> > > -              */
> > > -             dst_reg->s32_min_value = dst_reg->u32_min_value;
> > > -             dst_reg->s32_max_value = dst_reg->u32_max_value;
> > >       }
> > >  }
> >
> > [...]
> >
> > > @@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
> > >       /* We get both minimum and maximum from the var32_off. */
> > >       dst_reg->u32_min_value = var32_off.value;
> > >       dst_reg->u32_max_value = var32_off.value | var32_off.mask;
> > > -
> > > -     if (dst_reg->s32_min_value >= 0 && smin_val >= 0) {
> > > -             /* XORing two positive sign numbers gives a positive,
> > > -              * so safe to cast u32 result into s32.
> > > +     if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
> >
> > Same question here.
> >
> > > +             (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > > +             /* XORing two positives gives a positive, so safe to cast
> > > +              * u32 result into s32 when u32 doesn't cross sign boundary.
> > >                */
> > >               dst_reg->s32_min_value = dst_reg->u32_min_value;
> > >               dst_reg->s32_max_value = dst_reg->u32_max_value;
> >
> > [...]

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

[Harishankar Vishwanathan]

On Sat, Mar 30, 2024 at 1:28 AM Andrii Nakryiko
<andrii.nakryiko@gmail.com> wrote:
>
> On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
> <harishankar.vishwanathan@gmail.com> wrote:
> >
> > On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@gmail.com> 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.

> >
> > This applies to all scalar(32)_min_max_and/or/xor.
> >
> > > > +             (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > > > +             /* ORing two positives gives a positive, so safe to cast
> > > > +              * u32 result into s32 when u32 doesn't cross sign boundary.
> > > > +              */
> > > > +             dst_reg->s32_min_value = dst_reg->u32_min_value;
> > > > +             dst_reg->s32_max_value = dst_reg->u32_max_value;
> > > > +     } else {
> > > >               /* Lose signed bounds when ORing negative numbers,
> > > >                * ain't nobody got time for that.
> > > >                */
> > > >               dst_reg->s32_min_value = S32_MIN;
> > > >               dst_reg->s32_max_value = S32_MAX;
> > > > -     } else {
> > > > -             /* ORing two positives gives a positive, so safe to
> > > > -              * cast result into s64.
> > > > -              */
> > > > -             dst_reg->s32_min_value = dst_reg->u32_min_value;
> > > > -             dst_reg->s32_max_value = dst_reg->u32_max_value;
> > > >       }
> > > >  }
> > >
> > > [...]
> > >
> > > > @@ -13453,10 +13457,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
> > > >       /* We get both minimum and maximum from the var32_off. */
> > > >       dst_reg->u32_min_value = var32_off.value;
> > > >       dst_reg->u32_max_value = var32_off.value | var32_off.mask;
> > > > -
> > > > -     if (dst_reg->s32_min_value >= 0 && smin_val >= 0) {
> > > > -             /* XORing two positive sign numbers gives a positive,
> > > > -              * so safe to cast u32 result into s32.
> > > > +     if (dst_reg->s32_min_value > 0 && smin_val > 0 &&
> > >
> > > Same question here.
> > >
> > > > +             (s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
> > > > +             /* XORing two positives gives a positive, so safe to cast
> > > > +              * u32 result into s32 when u32 doesn't cross sign boundary.
> > > >                */
> > > >               dst_reg->s32_min_value = dst_reg->u32_min_value;
> > > >               dst_reg->s32_max_value = dst_reg->u32_max_value;
> > >
> > > [...]

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

[Daniel Borkmann]

On 3/30/24 5:35 PM, Harishankar Vishwanathan wrote:
> On Sat, Mar 30, 2024 at 1:28 AM Andrii Nakryiko
> <andrii.nakryiko@gmail.com> wrote:
>>
>> On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
>> <harishankar.vishwanathan@gmail.com> wrote:
>>>
>>> On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@gmail.com> 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

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

[Harishankar Vishwanathan]

On Tue, Apr 2, 2024 at 9:06 AM Daniel Borkmann <daniel@iogearbox.net> wrote:
>
> On 3/30/24 5:35 PM, Harishankar Vishwanathan wrote:
> > On Sat, Mar 30, 2024 at 1:28 AM Andrii Nakryiko
> > <andrii.nakryiko@gmail.com> wrote:
> >>
> >> On Fri, Mar 29, 2024 at 8:25 PM Harishankar Vishwanathan
> >> <harishankar.vishwanathan@gmail.com> wrote:
> >>>
> >>> On Fri, Mar 29, 2024 at 6:27 AM Eduard Zingerman <eddyz87@gmail.com> 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

Thanks Shung-Hsi, Eduard, Andrii, Daniel. I'll send over a new version
of the patch addressing
all the points discussed above.

Best,
Hari