netdev - Re: More BPF verifier questions

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <f75a8721-5cb0-f0bd-6224-b11bab1f036e@fb.com>
Date:   Mon, 5 Jun 2017 11:11:05 -0700
From:   Alexei Starovoitov <ast@...com>
To:     Edward Cree <ecree@...arflare.com>,
        Alexei Starovoitov <alexei.starovoitov@...il.com>,
        Daniel Borkmann <daniel@...earbox.net>
CC:     netdev <netdev@...r.kernel.org>,
        David Miller <davem@...emloft.net>,
        iovisor-dev <iovisor-dev@...ts.iovisor.org>,
        Josef Bacik <jbacik@...com>
Subject: Re: More BPF verifier questions

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?

> I tried to rewrite it to always base min_value on the signed and max_value
>  on the unsigned interpretation of the value (which, by looking at the sign
>  bit of the immediate, it can sometimes learn about the signed value from an
>  unsigned compare or vice versa), but this fails to validate e.g. test
>  "helper access to variable memory: stack, JMP (signed), correct bounds",
>  which first checks r2 s<= 64, then checks r2 s> 0.  If the checks were done
>  in the reverse order, we'd know when checking r2 s<= 64 that r2 is
>  positive, and that thus r2 u<= 64... but since we don't know that yet, when
>  we check r2 s<= 64 we learn nothing about r2's unsigned max_value.
> So, my current theory is that to do this right, we need to track four bounds
>  - s64 signed_min_value
>  - s64 signed_max_value
>  - u64 unsigned_min_value
>  - u64 unsigned_max_value

that would be unfortunate.
We already don't track negative values. Hence
BPF_REGISTER_MIN_RANGE = -1
so pretty much anything negative is rejected.
I don't think it worth complicating things for them.