2023-11-21 12:57:27

by Hao Sun

Subject: [Bug Report] bpf: reg invariant voilation after JSET

Hi,

The following program (reduced) breaks reg invariant:

C Repro: https://pastebin.com/raw/FmM9q9D4

-------- Verifier Log --------
func#0 @0
0: R1=ctx() R10=fp0
0: (18) r8 = 0x3d ; R8_w=61
2: (85) call bpf_ktime_get_ns#5 ; R0_w=scalar()
3: (ce) if w8 s< w0 goto pc+1 ; R0_w=scalar(smax32=61) R8_w=61
4: (95) exit

from 3 to 5: R0_w=scalar(smin=0x800000000000003e,smax=0x7fffffff7fffffff,umin=smin32=umin32=62,umax=0xffffffff7fffffff,umax32=0x7fffffff,var_off=(0x0;
0xffffffff7fffffff)) R8_w=61 R10=fp0
5: R0_w=scalar(smin=0x800000000000003e,smax=0x7fffffff7fffffff,umin=smin32=umin32=62,umax=0xffffffff7fffffff,umax32=0x7fffffff,var_off=(0x0;
0xffffffff7fffffff)) R8_w=61 R10=fp0
5: (45) if r0 & 0xfffffff7 goto pc+2
REG INVARIANTS VIOLATION (false_reg1): range bounds violation
u64=[0x3e, 0x8] s64=[0x3e, 0x8] u32=[0x3e, 0x8] s32=[0x3e, 0x8]
var_off=(0x0, 0x8)
5: R0_w=scalar(var_off=(0x0; 0x8))
6: (dd) if r0 s<= r8 goto pc+1
REG INVARIANTS VIOLATION (false_reg1): range bounds violation
u64=[0x0, 0x8] s64=[0x3e, 0x8] u32=[0x0, 0x8] s32=[0x0, 0x8]
var_off=(0x0, 0x8)
6: R0_w=scalar(var_off=(0x0; 0x8)) R8_w=61
7: (bc) w1 = w0 ; R0=scalar(var_off=(0x0; 0x8))
R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=8,var_off=(0x0; 0x8))
8: (95) exit

from 6 to 8: safe

from 5 to 8: safe
processed 10 insns (limit 1000000) max_states_per_insn 0 total_states
1 peak_states 1 mark_read 1

The tnum after #5 is correct, but the ranges are incorrect, which seems a bug in
reg_bounds_sync(). Thoughts?

Best
Hao Sun

2023-11-29 05:46:41

by Andrii Nakryiko

Subject: Re: [Bug Report] bpf: reg invariant voilation after JSET

On Tue, Nov 21, 2023 at 4:57 AM Hao Sun <[email protected]> wrote:
>
> Hi,
>
> The following program (reduced) breaks reg invariant:
>
> C Repro: https://pastebin.com/raw/FmM9q9D4
>
> -------- Verifier Log --------
> func#0 @0
> 0: R1=ctx() R10=fp0
> 0: (18) r8 = 0x3d ; R8_w=61
> 2: (85) call bpf_ktime_get_ns#5 ; R0_w=scalar()
> 3: (ce) if w8 s< w0 goto pc+1 ; R0_w=scalar(smax32=61) R8_w=61
> 4: (95) exit
>
> from 3 to 5: R0_w=scalar(smin=0x800000000000003e,smax=0x7fffffff7fffffff,umin=smin32=umin32=62,umax=0xffffffff7fffffff,umax32=0x7fffffff,var_off=(0x0;
> 0xffffffff7fffffff)) R8_w=61 R10=fp0
> 5: R0_w=scalar(smin=0x800000000000003e,smax=0x7fffffff7fffffff,umin=smin32=umin32=62,umax=0xffffffff7fffffff,umax32=0x7fffffff,var_off=(0x0;
> 0xffffffff7fffffff)) R8_w=61 R10=fp0
> 5: (45) if r0 & 0xfffffff7 goto pc+2
> REG INVARIANTS VIOLATION (false_reg1): range bounds violation
> u64=[0x3e, 0x8] s64=[0x3e, 0x8] u32=[0x3e, 0x8] s32=[0x3e, 0x8]
> var_off=(0x0, 0x8)
> 5: R0_w=scalar(var_off=(0x0; 0x8))
> 6: (dd) if r0 s<= r8 goto pc+1
> REG INVARIANTS VIOLATION (false_reg1): range bounds violation
> u64=[0x0, 0x8] s64=[0x3e, 0x8] u32=[0x0, 0x8] s32=[0x0, 0x8]
> var_off=(0x0, 0x8)
> 6: R0_w=scalar(var_off=(0x0; 0x8)) R8_w=61
> 7: (bc) w1 = w0 ; R0=scalar(var_off=(0x0; 0x8))
> R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=8,var_off=(0x0; 0x8))
> 8: (95) exit
>
> from 6 to 8: safe
>
> from 5 to 8: safe
> processed 10 insns (limit 1000000) max_states_per_insn 0 total_states
> 1 peak_states 1 mark_read 1
>
> The tnum after #5 is correct, but the ranges are incorrect, which seems a bug in
> reg_bounds_sync(). Thoughts?
>

It would be great if in addition to reporting the bug and repro
program, you could also try to analyse why this is happening and
suggest fixes in the verifier.

As I mentioned in another email, when we see REG INVARIANTS VIOLATION,
verifier reverts to conservative unknown scalar register state. We
should try to avoid this pessimistic outcome, but generally speaking
it should not be a critical bug.

> Best
> Hao Sun