Re: [RFC PATCH bpf-next 07/12] bpf/verifier: allow bounded loops with JLT/true back-edge

On 23/02/18 22:27, John Fastabend wrote:

On 02/23/2018 09:41 AM, Edward Cree wrote:

quoted

Where the register umin_value is increasing sufficiently fast, the loop
 will terminate after a reasonable number of iterations, so we can allow
 to keep walking it.

Continuing to walk the loop is problematic because we hit the complexity
limit. What we want to do is a static analysis step upfront on the basic
block containing the loop to ensure the loop is bounded.

We can do this by finding the induction variables (variables with form
cn+d) and ensuring the comparison register is an induction variable and
also increasing/decreasing correctly with respect to the comparison op.

This seems to be common in compilers to pull computation out of the
loop. So should be doable in the verifier.

So, I should mention that I _do_ have an idea for an optimisation that lets
 us avoid walking N times.  Basically, after you walk the loop for the first
 time (and detect the loop presence & jump condition), you change the type
 of the register from SCALAR_VALUE to INDUCTION_VARIABLE, which the other
 code should treat basically like a pointer in terms of accumulating offsets
 when doing arithmetic, etc.  Then when you get round the loop the second
 time, if the register still holds the INDUCTION_VARIABLE, you can look at
 the offsets and determine that the right thing is happening.  And because
 you made it around the loop with the INDUCTION_VARIABLE there, you know
 that any accesses etc. you do in the loop body are safe (you'd feed in the
 constraints you have in the min/max values so that e.g. array indexing could
 be verified).  So you do have to walk it twice, but not N times :-)
However, the idea needs more work to turn it into an obviously-correct
 algorithm (issues like nested loops and popped branches make me worry a
 little).
Also I feel a little safer knowing that if the verifier wrongly considers a
 loop bounded that actually isn't, it'll just walk round it until it hits the
 complexity limit and reject the program.  That seems like a nice kind of
 belt-and-braces security to have.

-Ed