bpf: Harden and/or/xor value tracking in verifier

This patch addresses a latent unsoundness issue in the
scalar(32)_min_max_and/or/xor functions. While it is not a bugfix,
it ensures that the functions produce sound outputs for all inputs.

The issue occurs in these functions 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 [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.

It is worth noting that while the previous code updated the signed bounds
(using the output unsigned bounds) only when the *input signed* bounds
were positive, the new code updates them whenever the *output unsigned*
bounds do not cross the sign boundary.

An alternative approach to fix this latent unsoundness would be to
unconditionally set the signed bounds to unbounded [S64_MIN, S64_MAX], and
let reg_bounds_sync() refine the signed bounds using the unsigned bounds
and the tnum. We found that our approach produces more precise (tighter)
bounds.

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_min_max_and()
produces:

  s32_min_value: -1263875629
  s32_max_value: -1

As observed, our patch produces a tighter s32 bound. We also confirmed
using Agni and SMT verification that our patch always produces signed
bounds that are equal to or more precise than setting the signed bounds to
unbounded in scalar_min_max_and().

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

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>
Signed-off-by: Daniel Borkmann <daniel@iogearbox.net>
Acked-by: Daniel Borkmann <daniel@iogearbox.net>
Link: https://lore.kernel.org/bpf/20240402212039.51815-1-harishankar.vishwanathan@gmail.com
Link: https://lore.kernel.org/bpf/20240416115303.331688-1-harishankar.vishwanathan@gmail.com

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 2aad6d90550f05780c2450f921a91a1b82a8a17b..68cfd6fc6ad4d389c2ad7103b99e983945325574 100644 (file)
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -13320,7 +13320,6 @@ static void scalar32_min_max_and(struct bpf_reg_state *dst_reg,
        bool src_known = tnum_subreg_is_const(src_reg->var_off);
        bool dst_known = tnum_subreg_is_const(dst_reg->var_off);
        struct tnum var32_off = tnum_subreg(dst_reg->var_off);
-       s32 smin_val = src_reg->s32_min_value;
        u32 umax_val = src_reg->u32_max_value;
 
        if (src_known && dst_known) {
@@ -13333,18 +13332,16 @@ 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) {
-               /* 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.
-                */
+
+       /* Safe to set s32 bounds by casting u32 result into s32 when u32
+        * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded.
+        */
+       if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
                dst_reg->s32_min_value = dst_reg->u32_min_value;
                dst_reg->s32_max_value = dst_reg->u32_max_value;
+       } else {
+               dst_reg->s32_min_value = S32_MIN;
+               dst_reg->s32_max_value = S32_MAX;
        }
 }
 
@@ -13353,7 +13350,6 @@ static void scalar_min_max_and(struct bpf_reg_state *dst_reg,
 {
        bool src_known = tnum_is_const(src_reg->var_off);
        bool dst_known = tnum_is_const(dst_reg->var_off);
-       s64 smin_val = src_reg->smin_value;
        u64 umax_val = src_reg->umax_value;
 
        if (src_known && dst_known) {
@@ -13366,18 +13362,16 @@ 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) {
-               /* 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.
-                */
+
+       /* Safe to set s64 bounds by casting u64 result into s64 when u64
+        * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded.
+        */
+       if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
                dst_reg->smin_value = dst_reg->umin_value;
                dst_reg->smax_value = dst_reg->umax_value;
+       } else {
+               dst_reg->smin_value = S64_MIN;
+               dst_reg->smax_value = S64_MAX;
        }
        /* We may learn something more from the var_off */
        __update_reg_bounds(dst_reg);
@@ -13389,7 +13383,6 @@ static void scalar32_min_max_or(struct bpf_reg_state *dst_reg,
        bool src_known = tnum_subreg_is_const(src_reg->var_off);
        bool dst_known = tnum_subreg_is_const(dst_reg->var_off);
        struct tnum var32_off = tnum_subreg(dst_reg->var_off);
-       s32 smin_val = src_reg->s32_min_value;
        u32 umin_val = src_reg->u32_min_value;
 
        if (src_known && dst_known) {
@@ -13402,18 +13395,16 @@ 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) {
-               /* 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.
-                */
+
+       /* Safe to set s32 bounds by casting u32 result into s32 when u32
+        * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded.
+        */
+       if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
                dst_reg->s32_min_value = dst_reg->u32_min_value;
                dst_reg->s32_max_value = dst_reg->u32_max_value;
+       } else {
+               dst_reg->s32_min_value = S32_MIN;
+               dst_reg->s32_max_value = S32_MAX;
        }
 }
 
@@ -13422,7 +13413,6 @@ static void scalar_min_max_or(struct bpf_reg_state *dst_reg,
 {
        bool src_known = tnum_is_const(src_reg->var_off);
        bool dst_known = tnum_is_const(dst_reg->var_off);
-       s64 smin_val = src_reg->smin_value;
        u64 umin_val = src_reg->umin_value;
 
        if (src_known && dst_known) {
@@ -13435,18 +13425,16 @@ 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) {
-               /* 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.
-                */
+
+       /* Safe to set s64 bounds by casting u64 result into s64 when u64
+        * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded.
+        */
+       if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
                dst_reg->smin_value = dst_reg->umin_value;
                dst_reg->smax_value = dst_reg->umax_value;
+       } else {
+               dst_reg->smin_value = S64_MIN;
+               dst_reg->smax_value = S64_MAX;
        }
        /* We may learn something more from the var_off */
        __update_reg_bounds(dst_reg);
@@ -13458,7 +13446,6 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
        bool src_known = tnum_subreg_is_const(src_reg->var_off);
        bool dst_known = tnum_subreg_is_const(dst_reg->var_off);
        struct tnum var32_off = tnum_subreg(dst_reg->var_off);
-       s32 smin_val = src_reg->s32_min_value;
 
        if (src_known && dst_known) {
                __mark_reg32_known(dst_reg, var32_off.value);
@@ -13469,10 +13456,10 @@ static void scalar32_min_max_xor(struct bpf_reg_state *dst_reg,
        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.
-                */
+       /* Safe to set s32 bounds by casting u32 result into s32 when u32
+        * doesn't cross sign boundary. Otherwise set s32 bounds to unbounded.
+        */
+       if ((s32)dst_reg->u32_min_value <= (s32)dst_reg->u32_max_value) {
                dst_reg->s32_min_value = dst_reg->u32_min_value;
                dst_reg->s32_max_value = dst_reg->u32_max_value;
        } else {
@@ -13486,7 +13473,6 @@ static void scalar_min_max_xor(struct bpf_reg_state *dst_reg,
 {
        bool src_known = tnum_is_const(src_reg->var_off);
        bool dst_known = tnum_is_const(dst_reg->var_off);
-       s64 smin_val = src_reg->smin_value;
 
        if (src_known && dst_known) {
                /* dst_reg->var_off.value has been updated earlier */
@@ -13498,10 +13484,10 @@ static void scalar_min_max_xor(struct bpf_reg_state *dst_reg,
        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.
-                */
+       /* Safe to set s64 bounds by casting u64 result into s64 when u64
+        * doesn't cross sign boundary. Otherwise set s64 bounds to unbounded.
+        */
+       if ((s64)dst_reg->umin_value <= (s64)dst_reg->umax_value) {
                dst_reg->smin_value = dst_reg->umin_value;
                dst_reg->smax_value = dst_reg->umax_value;
        } else {