More BPF verifier questions

* More BPF verifier questions
@ 2017-06-02 14:42 Edward Cree
       [not found] ` <24a519bc-d403-f429-5d72-2a1d31edfbe7-s/n/eUQHGBpZroRs9YW3xA@public.gmane.org>
  2017-06-05 18:11 ` Alexei Starovoitov
  0 siblings, 2 replies; 6+ messages in thread
From: Edward Cree @ 2017-06-02 14:42 UTC (permalink / raw)
  To: Alexei Starovoitov, Alexei Starovoitov, Daniel Borkmann
  Cc: netdev, David Miller, iovisor-dev

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.

^ permalink raw reply	[flat|nested] 6+ messages in thread