diff options
| author | Daniel Borkmann <daniel@iogearbox.net> | 2019-06-19 02:22:53 +0200 | 
|---|---|---|
| committer | Daniel Borkmann <daniel@iogearbox.net> | 2019-06-19 02:22:53 +0200 | 
| commit | 94079b64255fe40b9b53fd2e4081f68b9b14f54a (patch) | |
| tree | 2901e802c5161bb29dc5882fa14043f46de96cd0 /include/linux/bpf_verifier.h | |
| parent | a324aae32fa9bfdd03e89078e20ebcbd7737fda5 (diff) | |
| parent | b5dc0163d8fd78e64a7e21f309cf932fda34353e (diff) | |
| download | blackbird-op-linux-94079b64255fe40b9b53fd2e4081f68b9b14f54a.tar.gz blackbird-op-linux-94079b64255fe40b9b53fd2e4081f68b9b14f54a.zip | |
Merge branch 'bpf-bounded-loops'
Alexei Starovoitov says:
====================
v2->v3: fixed issues in backtracking pointed out by Andrii.
The next step is to add a lot more tests for backtracking.
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.
====================
Signed-off-by: Daniel Borkmann <daniel@iogearbox.net>
Diffstat (limited to 'include/linux/bpf_verifier.h')
| -rw-r--r-- | include/linux/bpf_verifier.h | 69 | 
1 files changed, 68 insertions, 1 deletions
| diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h index 704ed7971472..19393b0964a8 100644 --- a/include/linux/bpf_verifier.h +++ b/include/linux/bpf_verifier.h @@ -139,6 +139,8 @@ struct bpf_reg_state {  	 */  	s32 subreg_def;  	enum bpf_reg_liveness live; +	/* if (!precise && SCALAR_VALUE) min/max/tnum don't affect safety */ +	bool precise;  };  enum bpf_stack_slot_type { @@ -190,14 +192,77 @@ struct bpf_func_state {  	struct bpf_stack_state *stack;  }; +struct bpf_idx_pair { +	u32 prev_idx; +	u32 idx; +}; +  #define MAX_CALL_FRAMES 8  struct bpf_verifier_state {  	/* call stack tracking */  	struct bpf_func_state *frame[MAX_CALL_FRAMES]; +	struct bpf_verifier_state *parent; +	/* +	 * 'branches' field is the number of branches left to explore: +	 * 0 - all possible paths from this state reached bpf_exit or +	 * were safely pruned +	 * 1 - at least one path is being explored. +	 * This state hasn't reached bpf_exit +	 * 2 - at least two paths are being explored. +	 * This state is an immediate parent of two children. +	 * One is fallthrough branch with branches==1 and another +	 * state is pushed into stack (to be explored later) also with +	 * branches==1. The parent of this state has branches==1. +	 * The verifier state tree connected via 'parent' pointer looks like: +	 * 1 +	 * 1 +	 * 2 -> 1 (first 'if' pushed into stack) +	 * 1 +	 * 2 -> 1 (second 'if' pushed into stack) +	 * 1 +	 * 1 +	 * 1 bpf_exit. +	 * +	 * Once do_check() reaches bpf_exit, it calls update_branch_counts() +	 * and the verifier state tree will look: +	 * 1 +	 * 1 +	 * 2 -> 1 (first 'if' pushed into stack) +	 * 1 +	 * 1 -> 1 (second 'if' pushed into stack) +	 * 0 +	 * 0 +	 * 0 bpf_exit. +	 * After pop_stack() the do_check() will resume at second 'if'. +	 * +	 * If is_state_visited() sees a state with branches > 0 it means +	 * there is a loop. If such state is exactly equal to the current state +	 * it's an infinite loop. Note states_equal() checks for states +	 * equvalency, so two states being 'states_equal' does not mean +	 * infinite loop. The exact comparison is provided by +	 * states_maybe_looping() function. It's a stronger pre-check and +	 * much faster than states_equal(). +	 * +	 * This algorithm may not find all possible infinite loops or +	 * loop iteration count may be too high. +	 * In such cases BPF_COMPLEXITY_LIMIT_INSNS limit kicks in. +	 */ +	u32 branches;  	u32 insn_idx;  	u32 curframe;  	u32 active_spin_lock;  	bool speculative; + +	/* first and last insn idx of this verifier state */ +	u32 first_insn_idx; +	u32 last_insn_idx; +	/* jmp history recorded from first to last. +	 * backtracking is using it to go from last to first. +	 * For most states jmp_history_cnt is [0-3]. +	 * For loops can go up to ~40. +	 */ +	struct bpf_idx_pair *jmp_history; +	u32 jmp_history_cnt;  };  #define bpf_get_spilled_reg(slot, frame)				\ @@ -312,7 +377,9 @@ struct bpf_verifier_env {  	} cfg;  	u32 subprog_cnt;  	/* number of instructions analyzed by the verifier */ -	u32 insn_processed; +	u32 prev_insn_processed, insn_processed; +	/* number of jmps, calls, exits analyzed so far */ +	u32 prev_jmps_processed, jmps_processed;  	/* total verification time */  	u64 verification_time;  	/* maximum number of verifier states kept in 'branching' instructions */ | 

