BPF: bug without effect in BPF_RSH case of adjust_scalar_min_max_vals()

[Jann Horn]

As far as I can tell, commit b03c9f9fdc37 ("bpf/verifier: track signed
and unsigned min/max values") introduced the following effectless bug
in the BPF_RSH case of adjust_scalar_min_max_vals() (unless that's
intentional):

`dst_reg->smax_value` is only updated in the case where
`dst_reg->smin_value < 0` and `umin_val == 0`. This is obviously
harmless if `dst_reg->smax_value >= 0`, but if `dst_reg->smax_value <
0`, this will temporarily result in a state where the signed upper
bound of `dst_reg` is lower than the signed lower bound (which will be
set to 0). I don't think this should ever happen.

Luckily, this doesn't have any effect because of the
inter-representation information propagation that happens immediately
afterwards: __update_reg_bounds() neither modifies nor propagates the
incorrect `reg->smax_value` (the assignment is a no-op in this case),
then `__reg_deduce_bounds` takes the first branch and resets
`reg->smax_value` to `reg->umax_value`, which is correct.

To test this, I applied this patch to the kernel:

=======================
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index d4593571c404..bcf6a4aa25cd 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -2205,8 +2205,10 @@ static int adjust_scalar_min_max_vals(struct
bpf_verifier_env *env,
  dst_reg->var_off = tnum_rshift(tnum_unknown, umin_val);
  dst_reg->umin_value >>= umax_val;
  dst_reg->umax_value >>= umin_val;
+ pr_warn("BPF_RSH point A: smin=%lld, smax=%lld, umin=%llx,
umax=%llx, tribits=%llx, trimask=%llx\n", dst_reg->smin_value,
dst_reg->smax_value, dst_reg->umin_value, dst_reg->umax_value,
dst_reg->var_off.value, dst_reg->var_off.mask);
  /* We may learn something more from the var_off */
  __update_reg_bounds(dst_reg);
+ pr_warn("BPF_RSH point B: smin=%lld, smax=%lld, umin=%llx,
umax=%llx, tribits=%llx, trimask=%llx\n", dst_reg->smin_value,
dst_reg->smax_value, dst_reg->umin_value, dst_reg->umax_value,
dst_reg->var_off.value, dst_reg->var_off.mask);
  break;
  default:
  mark_reg_unknown(env, regs, insn->dst_reg);
@@ -2214,7 +2216,11 @@ static int adjust_scalar_min_max_vals(struct
bpf_verifier_env *env,
  }

  __reg_deduce_bounds(dst_reg);
+ if (opcode == BPF_RSH)
+ pr_warn("BPF_RSH point C: smin=%lld, smax=%lld, umin=%llx,
umax=%llx, tribits=%llx, trimask=%llx\n", dst_reg->smin_value,
dst_reg->smax_value, dst_reg->umin_value, dst_reg->umax_value,
dst_reg->var_off.value, dst_reg->var_off.mask);
  __reg_bound_offset(dst_reg);
+ if (opcode == BPF_RSH)
+ pr_warn("BPF_RSH point D: smin=%lld, smax=%lld, umin=%llx,
umax=%llx, tribits=%llx, trimask=%llx\n", dst_reg->smin_value,
dst_reg->smax_value, dst_reg->umin_value, dst_reg->umax_value,
dst_reg->var_off.value, dst_reg->var_off.mask);
  return 0;
 }
=======================

Then I attempted to load the following eBPF bytecode with verbosity level 2:

=======================
        BPF_LD_MAP_FD(BPF_REG_ARG1, mapfd),

        BPF_MOV64_REG(BPF_REG_TMP, BPF_REG_FP),
        BPF_ALU64_IMM(BPF_ADD, BPF_REG_TMP, -4), // allocate 4 bytes stack
        BPF_MOV32_IMM(BPF_REG_ARG2, 1),
        BPF_STX_MEM(BPF_W, BPF_REG_TMP, BPF_REG_ARG2, 0),
        BPF_MOV64_REG(BPF_REG_ARG2, BPF_REG_TMP),
        BPF_EMIT_CALL(BPF_FUNC_map_lookup_elem),
        BPF_JMP_IMM(BPF_JNE, BPF_REG_0, 0, 2),
        BPF_MOV64_REG(BPF_REG_0, 0), // prepare exit
        BPF_EXIT_INSN(), // exit
        BPF_LDX_MEM(BPF_W, BPF_REG_3, BPF_REG_0, 0),

        BPF_ALU64_IMM(BPF_AND, BPF_REG_3, 0xf),
        BPF_MOV64_IMM(BPF_REG_1, -42),
        BPF_ALU64_REG(BPF_ADD, BPF_REG_1, BPF_REG_3),
        BPF_MOV64_IMM(BPF_REG_2, 2),
        BPF_ALU64_REG(BPF_RSH, BPF_REG_1, BPF_REG_2),
        BPF_EXIT_INSN()
=======================

dmesg output:

=======================
[  145.423122] BPF_RSH point A: smin=0, smax=-27,
umin=3ffffffffffffff5, umax=3ffffffffffffff9,
tribits=3ffffffffffffff0, trimask=f
[  145.423129] BPF_RSH point B: smin=4611686018427387888, smax=-27,
umin=3ffffffffffffff5, umax=3ffffffffffffff9,
tribits=3ffffffffffffff0, trimask=f
[  145.423133] BPF_RSH point C: smin=4611686018427387893,
smax=4611686018427387897, umin=3ffffffffffffff5,
umax=3ffffffffffffff9, tribits=3ffffffffffffff0, trimask=f
[  145.423136] BPF_RSH point D: smin=4611686018427387893,
smax=4611686018427387897, umin=3ffffffffffffff5,
umax=3ffffffffffffff9, tribits=3ffffffffffffff0, trimask=f
=======================