On Mon, Dec 11, 2023 at 7:31 AM Hao Sun <sunhao.th@xxxxxxxxx> wrote: > > Hi, > > The verifier incorrectly prunes a path expected to be executed at > runtime. In the following program, the execution path is: > from 6 to 8 (taken) -> from 11 to 15 (taken) -> from 18 to 22 > (taken) -> from 26 to 27 (fall-through) -> from 29 to 30 > (fall-through) > The verifier prunes the checking path at #26, skipping the actual > execution path. > > 0: (18) r2 = 0x1a000000be > 2: (bf) r5 = r1 > 3: (bf) r8 = r2 > 4: (bc) w4 = w5 > 5: (85) call bpf_get_current_cgroup_id#680112 > 6: (36) if w8 >= 0x69 goto pc+1 > 7: (95) exit > 8: (18) r4 = 0x52 > 10: (84) w4 = -w4 > 11: (45) if r0 & 0xfffffffe goto pc+3 > 12: (1f) r8 -= r4 > 13: (0f) r0 += r0 > 14: (2f) r4 *= r4 > 15: (18) r3 = 0x1f00000034 > 17: (c4) w4 s>>= 29 > 18: (56) if w8 != 0xf goto pc+3 > 19: r3 = bswap32 r3 > 20: (18) r2 = 0x1c > 22: (67) r4 <<= 2 > 23: (bf) r5 = r8 > 24: (18) r2 = 0x4 > 26: (7e) if w8 s>= w0 goto pc+5 > 27: (4f) r8 |= r8 > 28: (0f) r8 += r8 > 29: (d6) if w5 s<= 0x1d goto pc+2 > 30: (18) r0 = 0x4 ; incorrectly pruned here > 32: (95) exit > > -------- Verifier Log -------- > func#0 @0 > 0: R1=ctx() R10=fp0 > 0: (18) r2 = 0x1a000000be ; R2_w=0x1a000000be > 2: (bf) r5 = r1 ; R1=ctx() R5_w=ctx() > 3: (bf) r8 = r2 ; R2_w=0x1a000000be R8_w=0x1a000000be > 4: (bc) w4 = w5 ; > R4_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff)) > R5_w=ctx() > 5: (85) call bpf_get_current_cgroup_id#80 ; R0_w=scalar() > 6: (36) if w8 >= 0x69 goto pc+1 > mark_precise: frame0: last_idx 6 first_idx 0 subseq_idx -1 > mark_precise: frame0: regs=r8 stack= before 5: (85) call > bpf_get_current_cgroup_id#80 > mark_precise: frame0: regs=r8 stack= before 4: (bc) w4 = w5 > mark_precise: frame0: regs=r8 stack= before 3: (bf) r8 = r2 > mark_precise: frame0: regs=r2 stack= before 2: (bf) r5 = r1 > mark_precise: frame0: regs=r2 stack= before 0: (18) r2 = 0x1a000000be > 6: R8_w=0x1a000000be > 8: (18) r4 = 0x52 ; R4_w=82 > 10: (84) w4 = -w4 ; R4=scalar() > 11: (45) if r0 & 0xfffffffe goto pc+3 ; > R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 12: (1f) r8 -= r4 ; R4=scalar() R8_w=scalar() > 13: (0f) r0 += r0 ; > R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) > 14: (2f) r4 *= r4 ; R4_w=scalar() > 15: (18) r3 = 0x1f00000034 ; R3_w=0x1f00000034 > 17: (c4) w4 s>>= 29 ; > R4_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) > 18: (56) if w8 != 0xf goto pc+3 ; > R8_w=scalar(smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; > 0xffffffff00000000)) > 19: (d7) r3 = bswap32 r3 ; R3_w=scalar() > 20: (18) r2 = 0x1c ; R2=28 > 22: (67) r4 <<= 2 ; > R4_w=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) > 23: (bf) r5 = r8 ; > R5_w=scalar(id=1,smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; > 0xffffffff00000000)) > R8=scalar(id=1,smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; > 0xffffffff00000000)) > 24: (18) r2 = 0x4 ; R2_w=4 > 26: (7e) if w8 s>= w0 goto pc+5 so here w8=15 and w0=[0,2], always taken, right? > mark_precise: frame0: last_idx 26 first_idx 22 subseq_idx -1 > mark_precise: frame0: regs=r5,r8 stack= before 24: (18) r2 = 0x4 > mark_precise: frame0: regs=r5,r8 stack= before 23: (bf) r5 = r8 > mark_precise: frame0: regs=r8 stack= before 22: (67) r4 <<= 2 > mark_precise: frame0: parent state regs=r8 stack=: > R0_rw=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R2_w=28 R3_w=scalar() > R4_rw=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) R8_rw=Pscalar(smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; > 0xffffffff00000000)) R10=fp0 > mark_precise: frame0: last_idx 20 first_idx 11 subseq_idx 22 > mark_precise: frame0: regs=r8 stack= before 20: (18) r2 = 0x1c > mark_precise: frame0: regs=r8 stack= before 19: (d7) r3 = bswap32 r3 > mark_precise: frame0: regs=r8 stack= before 18: (56) if w8 != 0xf goto pc+3 > mark_precise: frame0: regs=r8 stack= before 17: (c4) w4 s>>= 29 > mark_precise: frame0: regs=r8 stack= before 15: (18) r3 = 0x1f00000034 > mark_precise: frame0: regs=r8 stack= before 14: (2f) r4 *= r4 > mark_precise: frame0: regs=r8 stack= before 13: (0f) r0 += r0 > mark_precise: frame0: regs=r8 stack= before 12: (1f) r8 -= r4 > mark_precise: frame0: regs=r4,r8 stack= before 11: (45) if r0 & > 0xfffffffe goto pc+3 > mark_precise: frame0: parent state regs=r4,r8 stack=: R0_rw=scalar() > R4_rw=Pscalar() R8_rw=P0x1a000000be R10=fp0 > mark_precise: frame0: last_idx 10 first_idx 0 subseq_idx 11 > mark_precise: frame0: regs=r4,r8 stack= before 10: (84) w4 = -w4 > mark_precise: frame0: regs=r4,r8 stack= before 8: (18) r4 = 0x52 > mark_precise: frame0: regs=r8 stack= before 6: (36) if w8 >= 0x69 goto pc+1 > mark_precise: frame0: regs=r8 stack= before 5: (85) call > bpf_get_current_cgroup_id#80 > mark_precise: frame0: regs=r8 stack= before 4: (bc) w4 = w5 > mark_precise: frame0: regs=r8 stack= before 3: (bf) r8 = r2 > mark_precise: frame0: regs=r2 stack= before 2: (bf) r5 = r1 > mark_precise: frame0: regs=r2 stack= before 0: (18) r2 = 0x1a000000be > mark_precise: frame0: last_idx 26 first_idx 22 subseq_idx -1 > mark_precise: frame0: regs=r0 stack= before 24: (18) r2 = 0x4 > mark_precise: frame0: regs=r0 stack= before 23: (bf) r5 = r8 > mark_precise: frame0: regs=r0 stack= before 22: (67) r4 <<= 2 > mark_precise: frame0: parent state regs=r0 stack=: > R0_rw=Pscalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R2_w=28 R3_w=scalar() > R4_rw=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) R8_rw=Pscalar(smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; > 0xffffffff00000000)) R10=fp0 > mark_precise: frame0: last_idx 20 first_idx 11 subseq_idx 22 > mark_precise: frame0: regs=r0 stack= before 20: (18) r2 = 0x1c > mark_precise: frame0: regs=r0 stack= before 19: (d7) r3 = bswap32 r3 > mark_precise: frame0: regs=r0 stack= before 18: (56) if w8 != 0xf goto pc+3 > mark_precise: frame0: regs=r0 stack= before 17: (c4) w4 s>>= 29 > mark_precise: frame0: regs=r0 stack= before 15: (18) r3 = 0x1f00000034 > mark_precise: frame0: regs=r0 stack= before 14: (2f) r4 *= r4 > mark_precise: frame0: regs=r0 stack= before 13: (0f) r0 += r0 > mark_precise: frame0: regs=r0 stack= before 12: (1f) r8 -= r4 > mark_precise: frame0: regs=r0 stack= before 11: (45) if r0 & > 0xfffffffe goto pc+3 > mark_precise: frame0: parent state regs=r0 stack=: R0_rw=Pscalar() > R4_rw=Pscalar() R8_rw=P0x1a000000be R10=fp0 > mark_precise: frame0: last_idx 10 first_idx 0 subseq_idx 11 > mark_precise: frame0: regs=r0 stack= before 10: (84) w4 = -w4 > mark_precise: frame0: regs=r0 stack= before 8: (18) r4 = 0x52 > mark_precise: frame0: regs=r0 stack= before 6: (36) if w8 >= 0x69 goto pc+1 > mark_precise: frame0: regs=r0 stack= before 5: (85) call > bpf_get_current_cgroup_id#80 > 26: R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R8=scalar(id=1,smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; > 0xffffffff00000000)) > 32: (95) exit > > from 18 to 22: R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R3_w=0x1f00000034 > R4_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) R8_w=scalar() R10=fp0 > 22: R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R3_w=0x1f00000034 > R4_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) R8_w=scalar() R10=fp0 > 22: (67) r4 <<= 2 ; > R4_w=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) > 23: (bf) r5 = r8 ; R5_w=scalar(id=2) R8_w=scalar(id=2) > 24: (18) r2 = 0x4 ; R2=4 > 26: (7e) if w8 s>= w0 goto pc+5 ; > R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; 0x3)) > R8=scalar(id=2,smax32=1) we didn't prune here, assuming w8 < w0, so w8=w5 is at most 1 (because r0 is [0, 2]) > 27: (4f) r8 |= r8 ; R8_w=scalar() here r5 and r8 are disassociated > 28: (0f) r8 += r8 ; R8_w=scalar() > 29: (d6) if w5 s<= 0x1d goto pc+2 w5 is at most 1 (signed), so this is always true, so we just to exit, 30: is still never visited > mark_precise: frame0: last_idx 29 first_idx 26 subseq_idx -1 > mark_precise: frame0: regs=r5 stack= before 28: (0f) r8 += r8 > mark_precise: frame0: regs=r5 stack= before 27: (4f) r8 |= r8 > mark_precise: frame0: regs=r5 stack= before 26: (7e) if w8 s>= w0 goto pc+5 > mark_precise: frame0: parent state regs=r5 stack=: > R0_rw=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R2_w=4 R3_w=0x1f00000034 > R4_w=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) R5_rw=Pscalar(id=2) R8_rw=scalar(id=2) R10=fp0 > mark_precise: frame0: last_idx 24 first_idx 11 subseq_idx 26 > mark_precise: frame0: regs=r5,r8 stack= before 24: (18) r2 = 0x4 > mark_precise: frame0: regs=r5,r8 stack= before 23: (bf) r5 = r8 > mark_precise: frame0: regs=r8 stack= before 22: (67) r4 <<= 2 > mark_precise: frame0: regs=r8 stack= before 18: (56) if w8 != 0xf goto pc+3 > mark_precise: frame0: regs=r8 stack= before 17: (c4) w4 s>>= 29 > mark_precise: frame0: regs=r8 stack= before 15: (18) r3 = 0x1f00000034 > mark_precise: frame0: regs=r8 stack= before 14: (2f) r4 *= r4 > mark_precise: frame0: regs=r8 stack= before 13: (0f) r0 += r0 > mark_precise: frame0: regs=r8 stack= before 12: (1f) r8 -= r4 > mark_precise: frame0: regs=r4,r8 stack= before 11: (45) if r0 & > 0xfffffffe goto pc+3 > mark_precise: frame0: parent state regs= stack=: R0_rw=Pscalar() > R4_rw=Pscalar() R8_rw=P0x1a000000be R10=fp0 > 29: R5=scalar(id=2,smax32=1) > 32: (95) exit > > from 26 to 32: R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R2=4 R3=0x1f00000034 > R4=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) R5=scalar(id=2,smax=0x7fffffff7fffffff,umax=0xffffffff7fffffff,smin32=0,umax32=0x7fffffff,var_off=(0x0; > 0xffffffff7fffffff)) > R8=scalar(id=2,smax=0x7fffffff7fffffff,umax=0xffffffff7fffffff,smin32=0,umax32=0x7fffffff,var_off=(0x0; > 0xffffffff7fffffff)) R10=fp0 > 32: R0=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R2=4 R3=0x1f00000034 > R4=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) R5=scalar(id=2,smax=0x7fffffff7fffffff,umax=0xffffffff7fffffff,smin32=0,umax32=0x7fffffff,var_off=(0x0; > 0xffffffff7fffffff)) > R8=scalar(id=2,smax=0x7fffffff7fffffff,umax=0xffffffff7fffffff,smin32=0,umax32=0x7fffffff,var_off=(0x0; > 0xffffffff7fffffff)) R10=fp0 > 32: (95) exit here we also skipped 30:, and w8 was in [0,0x7fffffff] range, r0 is [0,2], but it's precision doesn't matter as we didn't do any pruning NOTE this one. > > from 11 to 15: R0=scalar() R4=scalar() R8=0x1a000000be R10=fp0 > 15: R0=scalar() R4=scalar() R8=0x1a000000be R10=fp0 > 15: (18) r3 = 0x1f00000034 ; R3_w=0x1f00000034 > 17: (c4) w4 s>>= 29 ; > R4=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) > 18: (56) if w8 != 0xf goto pc+3 known true, always taken > mark_precise: frame0: last_idx 18 first_idx 18 subseq_idx -1 > mark_precise: frame0: parent state regs=r8 stack=: R0=scalar() > R3_w=0x1f00000034 > R4_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) R8_r=P0x1a000000be R10=fp0 > mark_precise: frame0: last_idx 17 first_idx 11 subseq_idx 18 > mark_precise: frame0: regs=r8 stack= before 17: (c4) w4 s>>= 29 > mark_precise: frame0: regs=r8 stack= before 15: (18) r3 = 0x1f00000034 > mark_precise: frame0: regs=r8 stack= before 11: (45) if r0 & > 0xfffffffe goto pc+3 > mark_precise: frame0: parent state regs= stack=: R0_rw=Pscalar() > R4_rw=Pscalar() R8_rw=P0x1a000000be R10=fp0 > 18: R8=0x1a000000be > 22: (67) r4 <<= 2 ; > R4_w=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) > 23: (bf) r5 = r8 ; R5_w=0x1a000000be R8=0x1a000000be > 24: (18) r2 = 0x4 > frame 0: propagating r5 > mark_precise: frame0: last_idx 26 first_idx 18 subseq_idx -1 > mark_precise: frame0: regs=r5 stack= before 24: (18) r2 = 0x4 > mark_precise: frame0: regs=r5 stack= before 23: (bf) r5 = r8 > mark_precise: frame0: regs=r8 stack= before 22: (67) r4 <<= 2 > mark_precise: frame0: regs=r8 stack= before 18: (56) if w8 != 0xf goto pc+3 > mark_precise: frame0: parent state regs= stack=: R0_r=scalar() > R3_w=0x1f00000034 > R4_rw=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; > 0xffffffff)) R8_r=P0x1a000000be R10=fp0 > 26: safe and here we basically need to evaluate if w8 s>= w0 goto pc+5 w8 is precisely known to be 0x000000be, while w0 is unknown. Now go back to "NOTE this one" mark above. w8 is inside [0, 0xffffffff] range, right? And w0 is unknown, while up in "NOTE this one" w0 didn't matter, so it stayed imprecise. This is a match. It seems correct. > processed 38 insns (limit 1000000) max_states_per_insn 1 total_states > 4 peak_states 4 mark_read 2 > > -------- End of Verifier Log -------- > > When the verifier backtracks from #29, I expected w0 at #26 (if w8 s>= > w0 goto pc+5) to be marked as precise since R8 and R5 share the same > id: r0 is marked precise at 26: mark_precise: frame0: last_idx 26 first_idx 22 subseq_idx -1 mark_precise: frame0: regs=r0 stack= before 24: (18) r2 = 0x4 mark_precise: frame0: regs=r0 stack= before 23: (bf) r5 = r8 mark_precise: frame0: regs=r0 stack= before 22: (67) r4 <<= 2 mark_precise: frame0: parent state regs=r0 stack=: R0_rw=Pscalar(smin=smin32=0,sm ax=umax=smax32=umax32=2,var_off=(0x0; 0x3)) R2_w=28 R3_w=scalar() R4_rw=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=3,var_off=(0x0; 0xffffffff)) R8_rw=Pscalar(smin=0x800000000000000f,smax=0x7fffffff0000000f,umin=smin32=umin32=15,umax=0xffffffff0000000f,smax32=umax32=15,var_off=(0xf; 0xffffffff00000000)) R10=fp0 > > 29: (d6) if w5 s<= 0x1d goto pc+2 > mark_precise: frame0: last_idx 29 first_idx 26 subseq_idx -1 > mark_precise: frame0: regs=r5 stack= before 28: (0f) r8 += r8 > mark_precise: frame0: regs=r5 stack= before 27: (4f) r8 |= r8 > mark_precise: frame0: regs=r5 stack= before 26: (7e) if w8 s>= w0 goto pc+5 > mark_precise: frame0: parent state regs=r5 stack=: > R0_rw=scalar(smin=smin32=0,smax=umax=smax32=umax32=2,var_off=(0x0; > 0x3)) R2_w=4 R3_w=0x1f00000034 > R4_w=scalar(smin=0,smax=umax=0x3fffffffc,smax32=0x7ffffffc,umax32=0xfffffffc,var_off=(0x0; > 0x3fffffffc)) R5_rw=Pscalar(id=2) R8_rw=scalar(id=2) R10=fp0 > mark_precise: frame0: last_idx 24 first_idx 11 subseq_idx 26 > mark_precise: frame0: regs=r5,r8 stack= before 24: (18) r2 = 0x4 > mark_precise: frame0: regs=r5,r8 stack= before 23: (bf) r5 = r8 > mark_precise: frame0: regs=r8 stack= before 22: (67) r4 <<= 2 > mark_precise: frame0: regs=r8 stack= before 18: (56) if w8 != 0xf goto pc+3 > mark_precise: frame0: regs=r8 stack= before 17: (c4) w4 s>>= 29 > mark_precise: frame0: regs=r8 stack= before 15: (18) r3 = 0x1f00000034 > mark_precise: frame0: regs=r8 stack= before 14: (2f) r4 *= r4 > mark_precise: frame0: regs=r8 stack= before 13: (0f) r0 += r0 > mark_precise: frame0: regs=r8 stack= before 12: (1f) r8 -= r4 > mark_precise: frame0: regs=r4,r8 stack= before 11: (45) if r0 & > 0xfffffffe goto pc+3 > mark_precise: frame0: parent state regs= stack=: R0_rw=Pscalar() > R4_rw=Pscalar() R8_rw=P0x1a000000be R10=fp0 > 29: R5=scalar(id=2,smax32=1) > > However, seems it's not, so the next time when the verifier checks > #26, R0 is incorrectly ignored. > We have mark_precise_scalar_ids(), but it's called before calculating > the mask once. I'm not following the remark about mark_precise_scalar_ids(). That works fine, but has nothing to do with r0. mark_precise_scalar_ids() identifies that r8 and r5 are linked together, and you can see from the log that we mark both r5 and r8 as precise. > I investigated for quite a while, but mark_chain_pricision() is really > hard to follow. > > Here is a reduced C repro, maybe someone else can shed some light on this. > C repro: https://pastebin.com/raw/chrshhGQ So you claim is that 30: (18) r0 = 0x4 ; incorrectly pruned here Can you please show a detailed code patch in which we do reach 30 actually? I might have missed it, but so far it look like verifier is doing everything right. > > Thanks > Hao
