More BPF verifier questions

More BPF verifier questions

[Edward Cree]

A couple of the tests in tools/testing/selftests/bpf/test_verifier.c seem to be bogus: Test "multiple registers share map_lookup_elem bad reg type" is supposed to
 error with "R3 invalid mem access 'inv'", but from my reading of it, R3 gets
 loaded with a map_value_or_null, that later gets null-checked (both directly
 and - through R0 - indirectly), and finally stored through.  I don't see
 what's supposed to make R3 become a bad pointer.
Test "helper access to variable memory: stack, bitwise AND + JMP, correct
 bounds" is listed as expected to pass, but it passes zero in the 'size'
 argument, an ARG_CONST_SIZE, to bpf_probe_read; I believe this should fail
 (and with my WIP patch it does).
(Most of the tests that failed were for simple obvious reasons, like changes
 to the error messages or just being able to validate a construct that
 previously confused the verifier; I fix those in my patches.)

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 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
 and use all that information when updating the bounds after a cond jmp.
However, since the existing code didn't do that, but instead had some logic
 in reg_set_min_max[_inv] that I don't understand the reasoning behind, it's
 possible that I've missed something.

-Ed

PS. I'm getting near to having an RFC patch ready; it currently fails 13 of
 the tests in test_verifier.  I'd like to get that down to 0 before I post
 the patch, but if you'd prefer to see and review it before that point, just
 ask.

Re: More BPF verifier questions

[Y Song via iovisor-dev]

On Fri, Jun 2, 2017 at 7:42 AM, Edward Cree <ecree-s/n/eUQHGBpZroRs9YW3xA@public.gmane.org> wrote:
> A couple of the tests in tools/testing/selftests/bpf/test_verifier.c seem to be bogus: Test "multiple registers share map_lookup_elem bad reg type" is supposed to
>  error with "R3 invalid mem access 'inv'", but from my reading of it, R3 gets
>  loaded with a map_value_or_null, that later gets null-checked (both directly
>  and - through R0 - indirectly), and finally stored through.  I don't see
>  what's supposed to make R3 become a bad pointer.

You are right. In this case,
r0 = bpf_map_lookup
r2 = r0
r3 = r0
r4 = r0
r5 = r0
if (r0 != 0)  <=== condition 1
  r1 = 1
if (r0 != 0)
  r1 = 2
if (r3 != 0)
  *r3 = 0
...

If (r0 != 0) if false, the current verifier marks r2/r3/r4/r5 as unknown value.
I guess here what you did to have precise value 0 helps and make verifier
complaint go away correctly.

> Test "helper access to variable memory: stack, bitwise AND + JMP, correct
>  bounds" is listed as expected to pass, but it passes zero in the 'size'
>  argument, an ARG_CONST_SIZE, to bpf_probe_read; I believe this should fail
>  (and with my WIP patch it does).

Probably a typo or mis-statement. "size" is not passed in with "zero", but
with an unknown value. Hence, it probably should fail.

      BPF_MOV64_IMM(BPF_REG_2, 16),
      BPF_STX_MEM(BPF_DW, BPF_REG_1, BPF_REG_2, -128),
      BPF_LDX_MEM(BPF_DW, BPF_REG_2, BPF_REG_1, -128),
      BPF_ALU64_IMM(BPF_AND, BPF_REG_2, 64),
      BPF_MOV64_IMM(BPF_REG_4, 0),
      BPF_JMP_REG(BPF_JGE, BPF_REG_4, BPF_REG_2, 2),
      BPF_MOV64_IMM(BPF_REG_3, 0),
      BPF_EMIT_CALL(BPF_FUNC_probe_read),


In kernel/bpf/verifier.c,

  } else if (arg_type == ARG_CONST_SIZE ||
       arg_type == ARG_CONST_SIZE_OR_ZERO) {
    expected_type = CONST_IMM;
    /* One exception. Allow UNKNOWN_VALUE registers when the
     * boundaries are known and don't cause unsafe memory accesses
     */
    if (type != UNKNOWN_VALUE && type != expected_type)
      goto err_type;

Maybe somebody can provide some historical context for this relaxation.

Re: More BPF verifier questions

[Edward Cree]

On 05/06/17 08:06, Y Song wrote:
> On Fri, Jun 2, 2017 at 7:42 AM, Edward Cree <ecree@solarflare.com> wrote:
>> Test "helper access to variable memory: stack, bitwise AND + JMP, correct
>>  bounds" is listed as expected to pass, but it passes zero in the 'size'
>>  argument, an ARG_CONST_SIZE, to bpf_probe_read; I believe this should fail
>>  (and with my WIP patch it does).
> Probably a typo or mis-statement. "size" is not passed in with "zero", but
> with an unknown value. Hence, it probably should fail.
>
>       BPF_MOV64_IMM(BPF_REG_2, 16),
>       BPF_STX_MEM(BPF_DW, BPF_REG_1, BPF_REG_2, -128),
>       BPF_LDX_MEM(BPF_DW, BPF_REG_2, BPF_REG_1, -128),
>       BPF_ALU64_IMM(BPF_AND, BPF_REG_2, 64),
>       BPF_MOV64_IMM(BPF_REG_4, 0),
>       BPF_JMP_REG(BPF_JGE, BPF_REG_4, BPF_REG_2, 2),
>       BPF_MOV64_IMM(BPF_REG_3, 0),
>       BPF_EMIT_CALL(BPF_FUNC_probe_read),
So, in fact this unknown value is really 16 & 64 == 0, but the verifier doesn't
 know that and concludes that it's either 0 or 64 (after the AND).  But then
 what I didn't spot before, and now have, is that the BPF_JGE tests if 0 >= size.
 Since we're in the false branch, that means size > 0, and so we're fine.
The test case is correct, and now that I've fixed the min/max tracking in my
 patches, the verifier accepts it again.

-Ed

Re: More BPF verifier questions

[Alexei Starovoitov]

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.

Re: More BPF verifier questions

[Josef Bacik]

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

Re: More BPF verifier questions

[Edward Cree]

On 05/06/17 19:47, Josef Bacik wrote:
> On Mon, Jun 05, 2017 at 11:11:05AM -0700, Alexei Starovoitov wrote:
>> Do you have an asm test case that demonstrates that?
> 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,
Here's the basic idea:
    r1 = -8
    r2 = -1
    JGT r1, r2, end
    JSGT r1, 1, end
    ptr += r1
    *(u8 *)ptr = 0
After the JGT, we're in the false branch so r1->min_value = 0 and r1->max_value
 = (u64)-1.
After the JSGT, we're again in the false branch so r1->max_value = 1.
So when we add r1 to the pointer, the verifier thinks it's safe, but it's not,
 because r1 is really negative.

And here's the asm:
    BPF_ST_MEM(BPF_DW, BPF_REG_10, -8, 0),
    BPF_MOV64_REG(BPF_REG_2, BPF_REG_10),
    BPF_ALU64_IMM(BPF_ADD, BPF_REG_2, -8),
    BPF_LD_MAP_FD(BPF_REG_1, 0),
    BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0,
                 BPF_FUNC_map_lookup_elem),
    BPF_JMP_IMM(BPF_JEQ, BPF_REG_0, 0, 7),
    BPF_ST_MEM(BPF_DW, BPF_REG_10, -16, -8),
    BPF_LDX_MEM(BPF_DW, BPF_REG_1, BPF_REG_10, -16),
    BPF_MOV64_IMM(BPF_REG_2, -1),
    BPF_JMP_REG(BPF_JGT, BPF_REG_1, BPF_REG_2, 3),
    BPF_JMP_IMM(BPF_JSGT, BPF_REG_1, 1, 2),
    BPF_ALU64_REG(BPF_ADD, BPF_REG_0, BPF_REG_1),
    BPF_ST_MEM(BPF_B, BPF_REG_0, 0, 0),
    BPF_MOV64_IMM(BPF_REG_0, 0),
    BPF_EXIT_INSN(),
The verifier currently accepts this program (with an appropriate map fd), but I
 believe when run it will access invalid memory.

-Ed