netdev - Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

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: <935e538a-1400-cad0-c933-d4a200e5e0ef@fb.com>
Date:   Wed, 16 Nov 2016 15:25:01 -0500
From:   Josef Bacik <jbacik@...com>
To:     Jann Horn <jannh@...gle.com>
CC:     Alexei Starovoitov <alexei.starovoitov@...il.com>,
        Alexei Starovoitov <ast@...nel.org>,
        Daniel Borkmann <daniel@...earbox.net>,
        "David S. Miller" <davem@...emloft.net>, <netdev@...r.kernel.org>
Subject: Re: [PATCH net][v2] bpf: fix range arithmetic for bpf map access

On 11/16/2016 01:41 PM, Jann Horn wrote:
> On Tue, Nov 15, 2016 at 3:20 PM, Josef Bacik <jbacik@...com> wrote:
>> On 11/15/2016 08:47 AM, Jann Horn wrote:
>>> In states_equal():
>>> if (rold->type == NOT_INIT ||
>>>    (rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT))
>>> <------------
>>> continue;
>>>
>>> I think this is broken in code like the following:
>>>
>>> int value;
>>> if (condition) {
>>>   value = 1; // visited first by verifier
>>> } else {
>>>   value = 1000000; // visited second by verifier
>>> }
>>> int dummy = 1; // states seem to converge here, but actually don't
>>> map[value] = 1234;
>>>
>>> `value` would be an UNKNOWN_VALUE for both paths, right? So
>>> states_equal() would decide that the states converge after the
>>> conditionally executed code?
>>>
>>
>> Value would be CONST_IMM for both paths, and wouldn't match so they wouldn't
>> converge.  I think I understood your question right, let me know if I'm
>> addressing the wrong part of it.
>
> Okay, true, but what if you load the values from a map and bounds-check them
> instead of hardcoding them? Then they will be of type UNKNOWN_VALUE, right?
> Like this:
>
> int value = map[0];
> if (condition) {
>   value &= 0x1; // visited first by verifier
> } else {
>   // nothing; visited second by verifier
> }
> int dummy = 1; // states seem to converge here, but actually don't
> map[value] = 1234;
>
> And then `rold->type == UNKNOWN_VALUE && rcur->type != NOT_INIT` will be
> true in the `dummy = 1` line, and the states converge. Am I missing something?
>

Ah ok yeah I see it now you are right.  This is slightly different from this 
particular problem so I'll send a second patch to address this, sound 
reasonable?  Thanks,

Josef