check bpf_func_state->callback_depth when pruning states

The next commit in a series fixes bug in bpf_loop() handling. That change makes tcp_custom_syncookie test too complex to verify.

This commit updates tcp_custom_syncookie.c:tcp_parse_option() to use explicit packet offset (ctx->off) for packet access instead of ever moving pointer (ctx->ptr), this reduces verification complexity:
- the tcp_parse_option() is passed as a callback to bpf_loop();
- suppose a checkpoint is created each time at function entry;
- the ctx->ptr is tracked by verifier as PTR_TO_PACKET;
- the ctx->ptr is incremented in tcp_parse_option(),
thus umax_value field tracked for it is incremented as well;
- on each next iteration of tcp_parse_option()
checkpoint from a previous iteration can't be reused for state pruning, because PTR_TO_PACKET registers are considered equivalent only if old->umax_value >= cur->umax_value;
- on the other hand, the ctx->off is a SCALAR,
subject to widen_imprecise_scalars();
- it's exact bounds are eventually forgotten and it is tracked as unknown scalar at entry to tcp_parse_option();
- hence checkpoints created at the start of the function eventually converge.

The change is similar to one applied in [0] to xdp_synproxy_kern.c.

[0] commit 977bc146d4eb ("selftests/bpf: track tcp payload offset as scalar in xdp_synproxy")

Signed-off-by Eduard Zingerman <[email protected]>

When comparing current and cached states verifier should consider bpf_func_state->callback_depth. Current state cannot be pruned against cached state, when current states has more iterations left compared to cached state. Current state has more iterations left when it's callback_depth is smaller.

Below is an example illustrating this bug, minimized from mailing list discussion [0].
The example is not a safe program: if loop_cb point (1) is followed by loop_cb point (2), then division by zero is possible at point (4).

     struct ctx {
     	__u64 a;
     	__u64 b;
     	__u64 c;
     };

     static void loop_cb(int i, struct ctx *ctx)
     {
     	/* assume that generated code is "fallthrough-first":
     	 * if ... == 1 goto
     	 * if ... == 2 goto
     	 * <default>
     	 */
     	switch (bpf_get_prandom_u32()) {
     	case 1:  /* 1 */ ctx->a = 42; return 0; break;
     	case 2:  /* 2 */ ctx->b = 42; return 0; break;
     	default: /* 3 */ ctx->c = 42; return 0; break;
     	}
     }

     SEC("tc")
     __failure
     __flag(BPF_F_TEST_STATE_FREQ)
     int test(struct __sk_buff *skb)
     {

     	struct ctx ctx = { 7, 7, 7 };

     	bpf_loop(2, loop_cb, &ctx, 0);              /* 0 */
     	/* assume generated checks are in-order: .a first */
     	if (ctx.a == 42 && ctx.b == 42 && ctx.c == 7)
     		asm volatile("r0 /= 0;":::"r0");    /* 4 */
     	return 0;
     }

Prior to this commit verifier built the following checkpoint tree for this example (notation: (code point #) {<ctx->a>,<ctx->b>,<ctx->c>}):

- (0) {7P,7,7}

- (3) {7P,7,7}

- (0) {7P,7,42} (checkpoint #1):

- (3) {7P,7,42}
- (0) {7P,7,42} -> to end
- (2) {7P,7,42}
- (0) {7P,42,42} -> to end
- (1) {7P,7,42} (checkpoint #2)
- (0) {42P,7P,42} -> to end
- (2) {7P,7,7}

- (0) {7P,42,7} safe (checkpoint #1)
- (1) {7,7,7} safe (checkpoint #2)

Here checkpoint #2 has callback_depth of 1, meaning that it would never reach state {42,42,7}.

While the last branch of the tree has callback_depth of 0, and thus could yet explore the state {42,42,7} if not pruned prematurely.

This commit makes disallows such premature pruning.

[0] https://lore.kernel.org/bpf/[email protected]/

Suggested-by Yonghong Song <[email protected]>

Signed-off-by Eduard Zingerman <[email protected]>

---
  kernel/bpf/verifier.c | 3 +++
  1 file changed, 3 insertions(+)

kernel/bpf/verifier.c +3 -0

index ddaf09db1175..df99fcdbaa05 100644
@@ -16715,6 +16715,9 @@ static bool func_states_equal(struct bpf_verifier_env *env, struct bpf_func_stat
  {
  	int i;
 
+	if (old->callback_depth > cur->callback_depth)
+		return false;
+
  	for (i = 0; i < MAX_BPF_REG; i++)
  		if (!regsafe(env, &old->regs[i], &cur->regs[i],
  			     &env->idmap_scratch, exact))

Quoted 1 line

- (0) {7P,7,7}

Why we have '7P' here?

Quoted 1 line

- (3) {7P,7,7}

So here when (3) is hit, we have callback_depth  = 1, right?

Quoted 1 line

- (0) {7P,7,42} (checkpoint #1):

So for below (3)/(2)/(1) we have callback_depth = 2, right?

Quoted 7 lines

- (3) {7P,7,42}
- (0) {7P,7,42} -> to end
- (2) {7P,7,42}
- (0) {7P,42,42} -> to end
- (1) {7P,7,42} (checkpoint #2)
- (0) {42P,7P,42} -> to end
- (2) {7P,7,7}

So now we back to callback_depth = 1.

Quoted 2 lines

While the last branch of the tree has callback_depth of 0, and thus could yet explore the state {42,42,7} if not pruned prematurely.

which 'last branch'?

It would be good if the commit message mentions what will change for the above digram if this commit is applied, so people can understand why this commit helps.

Updated diagram with a few fixes, line numbers would be removed in the final version.

--- 8< ---------------------------------

.------------------------------------- Checkpoint / State name

  |    .-------------------------------- Code point number
  |    |   .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
  |    |   |        .------------------- Callback depth in frame #0
  v    v   v        v

1 - (0) {7P,7P,7},depth=0
2 - (3) {7P,7P,7},depth=1
3 - (0) {7P,7P,42},depth=1
(a) - (3) {7P,7,42},depth=2
4 - (0) {7P,7,42},depth=2 loop terminates because of depth limit
5 - (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
6 - (6) exit
7 - (2) {7P,7,42},depth=2
8 - (0) {7P,42,42},depth=2 loop terminates because of depth limit
9 - (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise

10 - (6) exit
(b) - (1) {7P,7P,42},depth=2
11 - (0) {42P,7P,42},depth=2 loop terminates because of depth limit
12 - (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
13 - (6) exit
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)

Here checkpoint (b) has callback_depth of 2, meaning that it would never reach state {42,42,7}.
While checkpoint (c) has callback_depth of 1, and thus could yet explore the state {42,42,7} if not pruned prematurely. This commit makes forbids such premature pruning, allowing verifier to explore states sub-tree starting at (c):

(c) - (1) {7,7,7P},depth=1
16 - (0) {42P,7,7P},depth=1

          ...

17 - (2) {42,7,7},depth=2
18 - (0) {42,42,7},depth=2 loop terminates because of depth limit
19 - (4) {42,42,7},depth=0 predicted true, ctx.{a,b,c} marked precise
20 - (5) division by zero

--------------------------------- >8 ---

Quoted 15 lines

.------------------------------------- Checkpoint / State name

  |    .-------------------------------- Code point number
  |    |   .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
  |    |   |        .------------------- Callback depth in frame #0
  v    v   v        v

1 - (0) {7P,7P,7},depth=0
2 - (3) {7P,7P,7},depth=1
3 - (0) {7P,7P,42},depth=1
(a) - (3) {7P,7,42},depth=2
4 - (0) {7P,7,42},depth=2 loop terminates because of depth limit
5 - (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
6 - (6) exit
7 - (2) {7P,7,42},depth=2
8 - (0) {7P,42,42},depth=2 loop terminates because of depth limit
9 - (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise

Quoted 8 lines

10 - (6) exit
(b) - (1) {7P,7P,42},depth=2
11 - (0) {42P,7P,42},depth=2 loop terminates because of depth limit
12 - (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
13 - (6) exit
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)

For the above line
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
I would change to
(c) - (1) {7P,7P,7},depth=1
- (0) {42P, 7P, 7},depth = 1 considered safe, pruned using checkpoint (11)

For
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
I suspect for line 15, the pruning uses checking point at line (8).

Other than the above, the diagram LGTM.

Quoted 23 lines · Yonghong Song

Quoted 15 lines

   .------------------------------------- Checkpoint / State name
   |    .-------------------------------- Code point number
   |    |   .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
   |    |   |        .------------------- Callback depth in frame #0
   v    v   v        v

1 - (0) {7P,7P,7},depth=0
2 - (3) {7P,7P,7},depth=1
3 - (0) {7P,7P,42},depth=1
(a) - (3) {7P,7,42},depth=2
4 - (0) {7P,7,42},depth=2 loop terminates because of depth limit
5 - (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
6 - (6) exit
7 - (2) {7P,7,42},depth=2
8 - (0) {7P,42,42},depth=2 loop terminates because of depth limit
9 - (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise

Quoted 8 lines

10 - (6) exit
(b) - (1) {7P,7P,42},depth=2
11 - (0) {42P,7P,42},depth=2 loop terminates because of depth limit
12 - (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
13 - (6) exit
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)

Quoted 5 lines

For the above line
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
I would change to
(c) - (1) {7P,7P,7},depth=1
- (0) {42P, 7P, 7},depth = 1 considered safe, pruned using checkpoint (11)

At that point:
- there is a checkpoint at (1) with state {7P,7P,42}
- verifier is at (1) in state {7,7,7}
Thus, verifier won't proceed to (0) because {7,7,7} is states_equal to {7P,7P,42}.

Quoted 5 lines

For
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
I suspect for line 15, the pruning uses checking point at line (8).

Right, because checkpoints for a particular insn form a stack. My bad.

Quoted 1 line

Other than the above, the diagram LGTM.

Thank you for the feedback, I'll post v2 shortly.

Quoted 30 lines · Eduard Zingerman

Quoted 28 lines · Yonghong Song

Quoted 15 lines

   .------------------------------------- Checkpoint / State name
   |    .-------------------------------- Code point number
   |    |   .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
   |    |   |        .------------------- Callback depth in frame #0
   v    v   v        v

1 - (0) {7P,7P,7},depth=0
2 - (3) {7P,7P,7},depth=1
3 - (0) {7P,7P,42},depth=1
(a) - (3) {7P,7,42},depth=2
4 - (0) {7P,7,42},depth=2 loop terminates because of depth limit
5 - (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
6 - (6) exit
7 - (2) {7P,7,42},depth=2
8 - (0) {7P,42,42},depth=2 loop terminates because of depth limit
9 - (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise

Quoted 8 lines

10 - (6) exit
(b) - (1) {7P,7P,42},depth=2
11 - (0) {42P,7P,42},depth=2 loop terminates because of depth limit
12 - (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
13 - (6) exit
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)

For the above line
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
I would change to
(c) - (1) {7P,7P,7},depth=1
- (0) {42P, 7P, 7},depth = 1 considered safe, pruned using checkpoint (11)

Quoted 4 lines

At that point:
- there is a checkpoint at (1) with state {7P,7P,42}
- verifier is at (1) in state {7,7,7}
Thus, verifier won't proceed to (0) because {7,7,7} is states_equal to {7P,7P,42}.

Okay, I think the above example has BPF_F_TEST_STATE_FREQ set as in Patch 3. It will be great if you can explicitly mention this (BPF_F_TEST_STATE_FREQ) in the commit message.

But then for
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
The state
14 - (2) {7P,7,7},depth=1
will have state equal to

    7        - (2) {7P,7,42},depth=2

right?