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
=======================
