Re: BUG in BPF verifier, 10 insns costs 2 mins+ to load

[Hao Sun]

Alexei Starovoitov <alexei.starovoitov@xxxxxxxxx> 于2022年11月8日周二 04:52写道：
>
> 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.
>

Hi,

Thanks for looking this.

No, `log_level` was set to 0 in this test. It takes more time if
enable verbose logging.
In this particular case, verifier should be able to exit at the first
time it meets BPF_JGT,
since R2=42 after insn 2, the test case essentially is like this:

0: r1 = 42
1: r2 = 0
2: r2 += r1
3: r2 /= 1 (alu32)
4: r1 -= 108
5: if r1 > r2 goto -3

But R2=42 was lost, after the following check for insn 3:

check_alu_op
  -> adjust_scalar_min_max_vals
         -> switch (op_code) {
             default:
               mark_reg_unknown(env, regs, insn->dst_reg);
               break;
             }

So, `dst_reg` range information is lost for both `BPF_DIV` and `BPF_MOD` insn.
I guess it's not easy to perform tracking over these ops in general
case, but should
we consider special cases like, devide by 1 and mod by 1, etc.

Also, I'm wondering if this behavior can be exploited, e.g., hind
actual value of particular
regs by deviding it by 1, then, trick verifier by adding a if
statement, finally, we get regs
with the value we want, something like this:

r0 = evil_val
r0 /= 1
if r0 > some_val goto X
at X:
verifier thinks r0 > some_val
but we know r0 equals evil_val

Just a random thought, no actual POC for this, any idea?

Regards
Hao

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