Re: [iovisor-dev] [PATCH v3 net-next 02/12] bpf/verifier: rework value tracking

[Edward Cree]

On 06/07/17 22:21, Nadav Amit wrote:
> I find it a bit surprising that such huge changes that can affect security
> and robustness are performed in one patch.
In the first version of the series, this was two patches, with "feed
 pointer-to-unknown-scalar casts into scalar ALU path" split out from the rest;
 but that just caused a lot of code movement and confusing diffs, hence why I
 folded it into the same patch.
As for the rest of it, I'm not sure it can be split up: I'm changing the
 definition and semantics of a core data structure (struct bpf_reg_state)
 and I don't see any reasonable intermediate steps that would even compile.
For instance, replacing reg->imm (with its two meanings of 'known value' or
 'number of leading zero bits') with reg->var_off necessitates replacing all
 the arithmetic-handling code (e.g. evaluate_reg_imm_alu()).  But then
 var_off also replaces reg->aux_align[_off], so all the alignment-checking
 code has to change as well.  And changing what register state we track
 means that the pruning code (states_equal()) has to change too.
As it is, this patch leaves some selftests failing and it takes _another_
 big patch (4/12 "track signed and unsigned min/max values") to get them
 all to pass again.
> Personally, I cannot comprehend
> all of these changes. In addition, I think that it is valuable to describe
> in detail the bugs that the patch solves and when they were introduced.
Mostly this patch series isn't about fixing bugs (except those which were
 exposed when the changes caused some selftests to fail).  Instead, it's a
 combination of refactoring and unifying so that (for instance) the rules
 for pointer arithmetic and alignment checking are as similar as possible
 for all pointer types rather than having special-case rules for each type.
This allows many (correct) programs which the verifier will currently
 reject, and makes the overall description of the verifier's rules much
 shorter and simpler.  I have written a documentation patch explaining
 these rules, which the next version of the patch series will include.

The diff _is_ hard to read, I accept that; I think `diff` was too eager to
 interpolate and match single lines like '{' from completely unrelated
 functions.  It might be easier to just try applying the patch to a tree
 and then reading the result, rather than trying to interpret the diff.
> I can bring up some concerns regarding inconsistencies in offset checks and
> size, not spilling SCALAR and my wish not to limit packet size. However,
> when the patch is that big, I think it is useless.
Please, do describe these concerns; what inconsistencies do you see?
The not spilling scalars, and the limit to packet size, are retained
 from the existing code (is_spillable_regtype() and MAX_PACKET_OFF).
The latter is also needed for correctness in computing reg->range;
 if 'pkt_ptr + offset' could conceivably overflow, then the result
 could be < pkt_end without being a valid pointer into the packet.
We thus rely on the assumption that the packet pointer will never be
 within MAX_PACKET_OFF of the top of the address space.  (This
 assumption is, again, carried over from the existing verifier.)

-Ed