From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-pf0-f175.google.com ([209.85.192.175]:43186 "EHLO mail-pf0-f175.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1751607AbeBWW1e (ORCPT ); Fri, 23 Feb 2018 17:27:34 -0500 Received: by mail-pf0-f175.google.com with SMTP id z14so4075104pfe.10 for ; Fri, 23 Feb 2018 14:27:34 -0800 (PST) Subject: Re: [RFC PATCH bpf-next 07/12] bpf/verifier: allow bounded loops with JLT/true back-edge To: Edward Cree , netdev , Alexei Starovoitov , Daniel Borkmann References: From: John Fastabend Message-ID: Date: Fri, 23 Feb 2018 14:27:18 -0800 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Language: en-US Content-Transfer-Encoding: 7bit Sender: netdev-owner@vger.kernel.org List-ID: On 02/23/2018 09:41 AM, Edward Cree wrote: > 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. > The semantics of prev_insn_idx are changed slightly: it now always refers > to the last jump insn walked, even when that jump was not taken. Also it > is moved into env, alongside a new bool last_jump_taken that records > whether the jump was taken or not. This is needed so that, when we detect > a loop, we can see how we ended up in the back-edge: what was the jump > condition, and is it the true- or the false-branch that ends up looping? > We record in our explored_states whether they represent a conditional jump > and whether that jump produced a good loop bound. This allows us to make > unconditional jumps "not responsible" for ensuring the loop is bounded, as > long as there is a conditional jump somewhere in the loop body; whereas a > conditional jump must ensure that there is a bounding conditional somewhere > in the loop body. > Recursive calls have to remain forbidden because the calculation of maximum > stack depth assumes the call graph is acyclic, even though the loop > handling code could determine whether the recursion was bounded. > > Signed-off-by: Edward Cree > ---