[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <CAG48ez2XnOQAc440ErNBATfL8uN1VOmV4M3BJKDW9s9PvWFOtg@mail.gmail.com>
Date: Wed, 16 Nov 2016 19:41:19 +0100
From: Jann Horn <jannh@...gle.com>
To: Josef Bacik <jbacik@...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 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?
Powered by blists - more mailing lists