[RFC PATCH 00/16] bpf, bounded loop support work in progress

* [RFC PATCH 00/16] bpf, bounded loop support work in progress
@ 2018-06-01  9:32 John Fastabend
  2018-06-01  9:32 ` [RFC PATCH 01/16] bpf: cfg: partition basic blocks for each subprog John Fastabend
                   ` (15 more replies)
  0 siblings, 16 replies; 17+ messages in thread
From: John Fastabend @ 2018-06-01  9:32 UTC (permalink / raw)
  To: alexei.starovoitov, daniel, davem; +Cc: netdev

This series is an early preview of ongoing work to support loops
inside BPF verifier. The code is rough in spots (more rough the
further you get into the series) but we have some signs of life!

The following code runs and is verified,

 SEC("classifier_tc_loop1")
 int _tc_loop(struct __sk_buff *ctx)
 {
	void *data      = (void *)(unsigned long)ctx->data;
	void *data_end  = (void *)(unsigned long)ctx->data_end;
	 __u8 i = 0, j = 0, k = 0, *p;

	 if (data + 2 > data_end)
		 return TC_ACT_OK;

	 p = data;
	 j = p[0];

	 if (data + 101 > data_end)
		 return TC_ACT_OK;

	 if (j < 100)
		 return TC_ACT_OK;

 #pragma nounroll
	while (i < j) {
		k += p[i];
		i++;
	}
	ctx->mark = k;

	return TC_ACT_OK;
 }

perhaps even more important many invalid loops are caught and
rejected. There are still a few cases that need to be handled
but largely things are working. And lots of code cleanup,
polishing and improvements sill needed but worth sharing
I think. Even if no one reads the code line by line the commit
messages have the description.

The series is broken into three parts.

Part1: Build the basic infrastruce. Basic Blocks, CFG and DOM are
built. (work done by Jiong).

Part2: Verify loops are bounded and encourage the state pruning
logic to prune as many states as possible.

Part3: Tests. Largely tbd at this point although I've been
doing lots of manual poking around with good/bad/ugly C programs.

Some high level details around design decisions for each part but
please see patch descriptions for more.

First Part1 Jiong chose to use Tarjan algorithm to build DOM.
(We also have an iterative solution if that is prefered but in
theory at least Tarjan has better running time.) Also we have
calculated the pdom as well but it is currently unused.

For all Part2 gory details please see patch,

 "bpf: verifier, add initial support to allow bounded loops"

The high level design is as follows,

  i. Use DOM to find loops
 ii. Find induction variables in loop
iii. Verify termination by comparing induction variable (inc/dec)
     against the JMP op. Propagate min/max values into insn aux
     data.
 iv. At do_check time ensure induction variable is bounded as
     required to ensure loop termination. These are a form of
     restriction on valid values for the registers.
  v. Encourage state pruning by using known bounds from
     previous induction step. e.g. if a scalar increments from
     0 to 100 we know min/max values that are vali for every
     iteration.
 vi. Loop state is usually pruned early but if not we can simply
     run the loop costing verifier complexity.

There is still lots of work to finish up all the pieces but we wanted
to share the current design.

Thanks,
John

---

Jiong Wang (11):
      bpf: cfg: partition basic blocks for each subprog
      bpf: cfg: add edges between basic blocks to form CFG
      bpf: cfg: build domination tree using Tarjan algorithm
      bpf: cfg: detect loop use domination information
      bpf: cfg: detect unreachable basic blocks
      bpf: cfg: move find_subprog/add_subprog to cfg.c
      bpf: cfg: build call graph and detect unreachable/recursive call
      bpf: cfg: remove push_insn and check_cfg
      bpf: cfg: reduce k*alloc/free call by using memory pool for allocating nodes
      bpf: cfg: reduce memory usage by using singly list + compat pointer
      bpf: cfg: detect irreducible loop using Eric Stoltz algorithm

John Fastabend (5):
      bpf: cfg: pretty print CFG and DOM
      bpf: verifier, can ptr range be calculated with scalar ALU op
      bpf: verifier, add initial support to allow bounded loops
      bpf: verifier, simple loop examples
      bpf: tools: dbg patch to turn on debugging and add primitive examples

 include/linux/bpf_verifier.h                   |   28 
 kernel/bpf/Makefile                            |    2 
 kernel/bpf/cfg.c                               | 2060 ++++++++++++++++++++++++
 kernel/bpf/cfg.h                               |   56 +
 kernel/bpf/verifier.c                          |  499 +++---
 samples/bpf/xdp2skb_meta_kern.c                |   57 +
 tools/lib/bpf/bpf.c                            |    2 
 tools/lib/bpf/libbpf.c                         |    7 
 tools/testing/selftests/bpf/Makefile           |    5 
 tools/testing/selftests/bpf/test_bad_loop1.c   |   47 +
 tools/testing/selftests/bpf/test_bad_loop2.c   |   45 +
 tools/testing/selftests/bpf/test_bad_loop3.c   |   47 +
 tools/testing/selftests/bpf/test_basic_loop1.c |   44 +
 tools/testing/selftests/bpf/test_basic_loop2.c |   48 +
 tools/testing/selftests/bpf/test_basic_loop3.c |   51 +
 15 files changed, 2711 insertions(+), 287 deletions(-)
 create mode 100644 kernel/bpf/cfg.c
 create mode 100644 kernel/bpf/cfg.h
 create mode 100644 tools/testing/selftests/bpf/test_bad_loop1.c
 create mode 100644 tools/testing/selftests/bpf/test_bad_loop2.c
 create mode 100644 tools/testing/selftests/bpf/test_bad_loop3.c
 create mode 100644 tools/testing/selftests/bpf/test_basic_loop1.c
 create mode 100644 tools/testing/selftests/bpf/test_basic_loop2.c
 create mode 100644 tools/testing/selftests/bpf/test_basic_loop3.c

^ permalink raw reply	[flat|nested] 17+ messages in thread