Re: [PATCH v3 bpf-next 0/9] bpf: bounded loops and other features

[Andrii Nakryiko <andrii.nakryiko@gmail.com>]

On Sat, Jun 15, 2019 at 12:12 PM Alexei Starovoitov <ast@kernel.org> wrote:
>
> v2->v3: fixed issues in backtracking pointed out by Andrii.
> The next step is to add a lot more tests for backtracking.
>

Tests would be great, verifier complexity is at the level, where it's
very easy to miss issues.

Was fuzzying approach ever discussed for BPF verifier? I.e., have a
fuzzer to generate both legal and illegal random small programs. Then
re-implement verifier as user-level program with straightforward
recursive exhaustive verification (so no state pruning logic, no
precise/coarse, etc, just register/stack state tracking) of all
possible branches. If kernel verifier's verdict differs from
user-level verifier's verdict - flag that as a test case and figure
out why they differ. Obviously that would work well only for small
programs, but that should be a good first step already.

In addition, if this is done, that user-land verifier can be a HUGE
help to BPF application developers, as libbpf would (potentially) be
able to generate better error messages using it as well.


> v1->v2: addressed Andrii's feedback.
>
> this patch set introduces verifier support for bounded loops and
> adds several other improvements.
> Ideally they would be introduced one at a time,
> but to support bounded loop the verifier needs to 'step back'
> in the patch 1. That patch introduces tracking of spill/fill
> of constants through the stack. Though it's a useful feature
> it hurts cilium tests.
> Patch 3 introduces another feature by extending is_branch_taken
> logic to 'if rX op rY' conditions. This feature is also
> necessary to support bounded loops.
> Then patch 4 adds support for the loops while adding
> key heuristics with jmp_processed.
> Introduction of parentage chain of verifier states in patch 4
> allows patch 9 to add backtracking of precise scalar registers
> which finally resolves degradation from patch 1.
>
> The end result is much faster verifier for existing programs
> and new support for loops.
> See patch 8 for many kinds of loops that are now validated.
> Patch 9 is the most tricky one and could be rewritten with
> a different algorithm in the future.
>
> Alexei Starovoitov (9):
>   bpf: track spill/fill of constants
>   selftests/bpf: fix tests due to const spill/fill
>   bpf: extend is_branch_taken to registers
>   bpf: introduce bounded loops
>   bpf: fix callees pruning callers
>   selftests/bpf: fix tests
>   selftests/bpf: add basic verifier tests for loops
>   selftests/bpf: add realistic loop tests
>   bpf: precise scalar_value tracking
>
>  include/linux/bpf_verifier.h                  |  69 +-
>  kernel/bpf/verifier.c                         | 767 ++++++++++++++++--
>  .../bpf/prog_tests/bpf_verif_scale.c          |  67 +-
>  tools/testing/selftests/bpf/progs/loop1.c     |  28 +
>  tools/testing/selftests/bpf/progs/loop2.c     |  28 +
>  tools/testing/selftests/bpf/progs/loop3.c     |  22 +
>  tools/testing/selftests/bpf/progs/pyperf.h    |   6 +-
>  tools/testing/selftests/bpf/progs/pyperf600.c |   9 +
>  .../selftests/bpf/progs/pyperf600_nounroll.c  |   8 +
>  .../testing/selftests/bpf/progs/strobemeta.c  |  10 +
>  .../testing/selftests/bpf/progs/strobemeta.h  | 528 ++++++++++++
>  .../bpf/progs/strobemeta_nounroll1.c          |   9 +
>  .../bpf/progs/strobemeta_nounroll2.c          |   9 +
>  .../selftests/bpf/progs/test_seg6_loop.c      | 261 ++++++
>  .../selftests/bpf/progs/test_sysctl_loop1.c   |  71 ++
>  .../selftests/bpf/progs/test_sysctl_loop2.c   |  72 ++
>  .../selftests/bpf/progs/test_xdp_loop.c       | 231 ++++++
>  tools/testing/selftests/bpf/test_verifier.c   |  11 +-
>  tools/testing/selftests/bpf/verifier/calls.c  |  22 +-
>  tools/testing/selftests/bpf/verifier/cfg.c    |  11 +-
>  .../bpf/verifier/direct_packet_access.c       |   3 +-
>  .../bpf/verifier/helper_access_var_len.c      |  28 +-
>  tools/testing/selftests/bpf/verifier/loops1.c | 161 ++++
>  23 files changed, 2317 insertions(+), 114 deletions(-)
>  create mode 100644 tools/testing/selftests/bpf/progs/loop1.c
>  create mode 100644 tools/testing/selftests/bpf/progs/loop2.c
>  create mode 100644 tools/testing/selftests/bpf/progs/loop3.c
>  create mode 100644 tools/testing/selftests/bpf/progs/pyperf600.c
>  create mode 100644 tools/testing/selftests/bpf/progs/pyperf600_nounroll.c
>  create mode 100644 tools/testing/selftests/bpf/progs/strobemeta.c
>  create mode 100644 tools/testing/selftests/bpf/progs/strobemeta.h
>  create mode 100644 tools/testing/selftests/bpf/progs/strobemeta_nounroll1.c
>  create mode 100644 tools/testing/selftests/bpf/progs/strobemeta_nounroll2.c
>  create mode 100644 tools/testing/selftests/bpf/progs/test_seg6_loop.c
>  create mode 100644 tools/testing/selftests/bpf/progs/test_sysctl_loop1.c
>  create mode 100644 tools/testing/selftests/bpf/progs/test_sysctl_loop2.c
>  create mode 100644 tools/testing/selftests/bpf/progs/test_xdp_loop.c
>  create mode 100644 tools/testing/selftests/bpf/verifier/loops1.c
>
> --
> 2.20.0
>