On 12/01/18 19:23, Daniel Borkmann wrote: > syzkaller generated a BPF proglet and triggered a warning with > the following: > > 0: (b7) r0 = 0 > 1: (d5) if r0 s<= 0x0 goto pc+0 > R0=inv0 R1=ctx(id=0,off=0,imm=0) R10=fp0 > 2: (1f) r0 -= r1 > R0=inv0 R1=ctx(id=0,off=0,imm=0) R10=fp0 > verifier internal error: known but bad sbounds > > What happens is that in the first insn, r0's min/max value are > both 0 due to the immediate assignment, later in the jsle test > the bounds are updated for the min value in the false path, > meaning, they yield smin_val = 1 smax_val = 0, reg_set_min_max() refines the existing bounds, it doesn't replace them, so all that's happened is that the jsle handling has demonstrated that this branch can't be taken. That AFAICT isn't confined to known constants, one could e.g. obtain inconsistent bounds with two js* insns. Updating the bounds in reg_set_min_max() is right, it's where we try to use those sbounds in adjust_ptr_min_max_vals() that's wrong imho; instead the 'known' paths should be using off_reg->var_off.value rather than smin_val everywhere.
Alternatively we could consider not following jumps/lack-thereof that produce inconsistent bounds, but that can make insns unreachable that previously weren't and thus reject programs that we previously considered valid, so we probably can't get away with that. -Ed
