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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <abb7c828-fc0f-4279-0b8c-cc70a076e88c@gmail.com>
Date:   Fri, 23 Feb 2018 14:27:18 -0800
From:   John Fastabend <john.fastabend@...il.com>
To:     Edward Cree <ecree@...arflare.com>,
        netdev <netdev@...r.kernel.org>,
        Alexei Starovoitov <ast@...nel.org>,
        Daniel Borkmann <daniel@...earbox.net>
Subject: Re: [RFC PATCH bpf-next 07/12] bpf/verifier: allow bounded loops with
 JLT/true back-edge

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 <ecree@...arflare.com>
> ---