On Sun, Nov 6, 2022 at 8:26 PM Hao Sun <sunhao.th@xxxxxxxxx> wrote: > > Hi, > > I've just written a BPF verifier fuzzer, targeting logic bugs in the > BPF verifier. > The following is an abnormal case it generated. The case only contains 10 > BPF instructions but costs more than 2 mins to load on : with full verbose verifier logging, right? That is expected for any prog that is going to hit the 1M insn limit. > HEAD commit: f0c4d9fc9cc9 Linux 6.1-rc4 > git tree: upstream > kernel config: https://pastebin.com/raw/SBxaikiG > C reproducer: https://pastebin.com/raw/HsDXdraZ > verifier log: https://pastebin.com/raw/sNmSsVxs > > Ideally, the verifier should exit quickly in this case, since R2=42 > always holds. > The behaviour of the verifier does not make sense to me, seems it lost > the range information of R2. > > Please point out if I missed anything, the C reproducer in the link > (https://pastebin.com/raw/HsDXdraZ) > essentially loads the following case into `test_verifier.c`: > { > "BVF verifier test", > .insns = { > BPF_MOV64_IMM(BPF_REG_1, 42), > BPF_MOV64_IMM(BPF_REG_2, 0), > BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 1, 0, 1), > BPF_EXIT_INSN(), > BPF_ALU64_REG(BPF_ADD, BPF_REG_2, BPF_REG_1), > BPF_ALU32_IMM(BPF_DIV, BPF_REG_2, 1), > BPF_ALU64_IMM(BPF_SUB, BPF_REG_1, 108), > BPF_JMP32_REG(BPF_JGT, BPF_REG_1, BPF_REG_2, -3), > BPF_MOV64_REG(BPF_REG_0, BPF_REG_2), > BPF_EXIT_INSN(), > }, > .prog_type = BPF_PROG_TYPE_XDP, > }, > > The verifier's log is more then 4M, but essentially is: > 0: R1=ctx(off=0,imm=0) R10=fp0 > 0: (b7) r1 = 42 ; R1_w=P42 > 1: (b7) r2 = 0 ; R2_w=P0 > 2: (85) call pc+1 > caller: > R10=fp0 > callee: > frame1: R1_w=P42 R2_w=P0 R10=fp0 > 4: (57) r2 &= -52 ; frame1: R2_w=P0 > 5: (0f) r2 += r1 ; frame1: R1_w=P42 R2_w=P42 > 6: (34) w2 /= 1 ; frame1: > R2_w=Pscalar(umax=4294967295,var_off=(0x0; 0xffffffff)) > 7: (17) r1 -= 108 ; frame1: R1_w=P-66 > 8: (2e) if w1 > w2 goto pc-3 6: frame1: R1_w=P-66 > R2_w=Pscalar(umax=4294967229,var_off=(0x0; 0xffffffff)) R10=fp0 > 6: (34) w2 /= 1 ; frame1: > R2_w=Pscalar(umax=4294967295,var_off=(0x0; 0xffffffff)) > 7: (17) r1 -= 108 ; frame1: R1_w=P-174 > 8: (2e) if w1 > w2 goto pc-3 6: frame1: R1_w=P-174 > R2_w=Pscalar(umax=4294967121,var_off=(0x0; 0xffffffff)) R10=fp0 > 6: (34) w2 /= 1 ; frame1: > R2_w=Pscalar(umax=4294967295,var_off=(0x0; 0xffffffff)) > 7: (17) r1 -= 108 ; frame1: R1=P-282 > 8: (2e) if w1 > w2 goto pc-3 6: frame1: R1=P-282 > R2=Pscalar(umax=4294967013,var_off=(0x0; 0xffffffff)) R10=fp0 > ... > 6: (34) w2 /= 1 ; frame1: > R2_w=Pscalar(umax=4294967295,var_off=(0x0; 0xffffffff)) > 7: (17) r1 -= 108 ; frame1: R1_w=P-6342690 > 8: (2e) if w1 > w2 goto pc-3 6: frame1: R1_w=P-6342690 > R2_w=Pscalar(umax=4288624605,var_off=(0x0; 0xffffffff)) R10=fp0 > 6: (34) w2 /= 1 ; frame1: > R2_w=Pscalar(umax=4294967295,var_off=(0x0; 0xffffffff)) > 7: (17) r1 -= 108 ; frame1: R1_w=P-6342798 > 8: (2e) if w1 > w2 goto pc-3 ; frame1: R1_w=P-6342798 > R2_w=Pscalar(umin=4288624498,umax=4294967295,var_off=(0xff800000; > 0x7fffff),s32_min=-6342798,s32_max=-1) > 9: (bf) r0 = r2 ; frame1: > R0_w=Pscalar(id=58730,umin=4288624498,umax=4294967295,var_off=(0xff800000; > 0x7fffff),s32_min=-6342798,s32_max=-1) > R2_w=Pscalar(id=58730,umin=4288624498,umax=4294967295,var_off=(0xff800000; > 0x7fffff),s32_min=-6342798,s32_max=-1) > 10: (95) exit > returning from callee: > frame1: R0_w=Pscalar(id=58730,umin=4288624498,umax=4294967295,var_off=(0xff800000; > 0x7fffff),s32_min=-6342798,s32_max=-1) R1_w=P-6342798 > R2_w=Pscalar(id=58730,umin=4288624498,umax=4294967295,var_off=(0xff800000; > 0x7fffff),s32_min=-6342798,s32_max=-1) R10=fp0 > to caller at 3: > R0_w=Pscalar(id=58730,umin=4288624498,umax=429496
