Re: More BPF verifier questions

[Josef Bacik <josef@toxicpanda.com>]

On Mon, Jun 05, 2017 at 11:11:05AM -0700, Alexei Starovoitov wrote:
> On 6/2/17 7:42 AM, Edward Cree wrote:
> >Also, I feel I haven't fully understood the semantics of {min,max}_value and
> > signed vs. unsigned comparisons.  It seems that currently reg_set_min_max
> > [_inv] assumes that any given register-value will either only be used as
> > signed, or only be used as unsigned — which while potentially reasonable
> > for compiler-generated bytecode, could easily be untrue of a hand-crafted
> > BPF program.
> >For instance, take BPF_JGT(reg, val).  This currently sets
> > false_reg->min_value to zero, but if val >= (1<<63), the false branch could
> > be taken for a value that's negative (when interpreted as signed).
> 
> I think the way Josef intended it to behave is min/max_value are
> absolute values that 64-bits can hold.
> In that sense unsigned (JGT) comparison and the false branch are
> implying that min_value = 0.
> but if we don't treat min/max consistently as sign-free numbers
> than indeed it can cause issues.
> Do you have an asm test case that demonstrates that?
>

Well the min_value is a s64, but yeah anything negative is supposed to be
rejected, so it essentially acts as the range of unsigned absolute values it can
hold.  I tried to hand craft a way to exploit this but I don't think it's
possible.  In the normal BPF_JGT path with your case we'd end up with

false_reg->min_value = 0;
false_reg->max_value = 1<<63 = BPF_REGISTER_MAX_RANGE
true_reg->min_value = BPF_REGISTER_MIN_RANGE

>From here we want to exploit the fact that false_reg->min_value is not
necessarily correct, but in order to do that we need to get false_reg->max_value
below the actual size limit for the data we're reaching into, which means we
want to _only_ change false_reg->max_value.  Thankfully there doesn't appear to
be a way to do that, everything changes either only min_value or both min_value
and max_value.  I think we're safe here, unless I've missed something.  Thanks,

Josef