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
--
Signature
