• Alexei Starovoitov's avatar
    bpf: add search pruning optimization to verifier · f1bca824
    Alexei Starovoitov authored
    consider C program represented in eBPF:
    int filter(int arg)
    {
        int a, b, c, *ptr;
    
        if (arg == 1)
            ptr = &a;
        else if (arg == 2)
            ptr = &b;
        else
            ptr = &c;
    
        *ptr = 0;
        return 0;
    }
    eBPF verifier has to follow all possible paths through the program
    to recognize that '*ptr = 0' instruction would be safe to execute
    in all situations.
    It's doing it by picking a path towards the end and observes changes
    to registers and stack at every insn until it reaches bpf_exit.
    Then it comes back to one of the previous branches and goes towards
    the end again with potentially different values in registers.
    When program has a lot of branches, the number of possible combinations
    of branches is huge, so verifer has a hard limit of walking no more
    than 32k instructions. This limit can be reached and complex (but valid)
    programs could be rejected. Therefore it's important to recognize equivalent
    verifier states to prune this depth first search.
    
    Basic idea can be illustrated by the program (where .. are some eBPF insns):
        1: ..
        2: if (rX == rY) goto 4
        3: ..
        4: ..
        5: ..
        6: bpf_exit
    In the first pass towards bpf_exit the verifier will walk insns: 1, 2, 3, 4, 5, 6
    Since insn#2 is a branch the verifier will remember its state in verifier stack
    to come back to it later.
    Since insn#4 is marked as 'branch target', the verifier will remember its state
    in explored_states[4] linked list.
    Once it reaches insn#6 successfully it will pop the state recorded at insn#2 and
    will continue.
    Without search pruning optimization verifier would have to walk 4, 5, 6 again,
    effectively simulating execution of insns 1, 2, 4, 5, 6
    With search pruning it will check whether state at #4 after jumping from #2
    is equivalent to one recorded in explored_states[4] during first pass.
    If there is an equivalent state, verifier can prune the search at #4 and declare
    this path to be safe as well.
    In other words two states at #4 are equivalent if execution of 1, 2, 3, 4 insns
    and 1, 2, 4 insns produces equivalent registers and stack.
    Signed-off-by: default avatarAlexei Starovoitov <ast@plumgrid.com>
    Signed-off-by: default avatarDavid S. Miller <davem@davemloft.net>
    f1bca824
verifier.c 52.5 KB