bpf: incorrect range tracking on JE and JNE with non-overlap ranges

From: Hao Sun
Date: Sun Nov 12 2023 - 12:46:01 EST


Hi,

Currently, the verifier collects incorrect ranges on the fall-through
of JNE and the branch-taken of JE when ranges of their operands are
non-overlap. The following program can trigger a shift out of bounds
on the fall-through of the JNE path.

C Program: https://pastebin.com/raw/CKvS707A
Shift-out-of-bound: https://pastebin.com/raw/AkJWxVue
Verifier Log: https://pastebin.com/raw/fdjG3u61

In the C program, r7 and r1 have different ranges and are compared:

12: (bf) r4 = r0 ;
R0_w=scalar(id=2,smin=smin32=-4,smax=smax32=-1,umin=18446744073709551612,umin32=4294967292,var_off=(0xfffffffffffffffc;
0x3)) R4_w=scalar(id=2,smin=smin32=-4,smax=smax32=-1,umin=18446744073709551612,umin32=4294967292,var_off=(0xfffffffffffffffc;
0x3))
13: (bf) r6 = r7 ;
R6=scalar(id=3,smin=smin32=0,smax=umax=smax32=umax32=24,var_off=(0x0;
0x18)) R7=scalar(id=3,smin=smin32=0,smax=umax=smax32=umax32=24,var_off=(0x0;
0x18))
14: (5d) if r7 != r0 goto pc+2 ; R0=-4 R7=-4

The issue is that is_branch_taken() requires one of the regs to be
known/const, and it returns -1 even when the ranges are non-overlap.
Later, reg_combine_min_max() is called, which assumes two regs could
equal. So, when two ranges are non-overlap, the range of the
corresponding eq path of JE and JNE is incorrect:

if (dst_reg->type == SCALAR_VALUE &&
src_reg->type == SCALAR_VALUE &&
!is_jmp32 && (opcode == BPF_JEQ || opcode == BPF_JNE)) {
/* Comparing for equality, we can combine knowledge */
reg_combine_min_max(&other_branch_regs[insn->src_reg],
&other_branch_regs[insn->dst_reg],
src_reg, dst_reg, opcode);
}

Andrii's patch sets fixed similar issues
(https://lore.kernel.org/bpf/CAEf4Bzbgf-WQSCz8D4Omh3zFdS4oWS6XELnE7VeoUWgKf3cpig@xxxxxxxxxxxxxx/)
where ranges are non-overlap, but one of the subreg is known.

Report this one since this case seems different from the previous one,
and still triggers issues on the latest bpf-next. Also, the range
tracking of non-overlap const/range for JSLT is not correct either,
see my previous report:
https://lore.kernel.org/bpf/CACkBjsbvk7rNfV0uS8uvrw497ybB1uLvUFvZWPx_SBzSRn2Raw@xxxxxxxxxxxxxx/