[PATCH bpf-next 0/3] check bpf_func_state->callback_depth when pruning states

[PATCH bpf-next 0/3] check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman]

This patch-set fixes bug in states pruning logic hit in mailing list
discussion [0]. The details of the fix are in patch #2.
A change to the test case test_tcp_custom_syncookie.c is necessary,
otherwise updated verifier won't be able to process it due to
instruction complexity limit. This change is done in patch #1.

The main idea for the fix belongs to Yonghong Song,
mine contribution is merely in review and test cases.

[0] https://lore.kernel.org/bpf/9b251840-7cb8-4d17-bd23-1fc8071d8eef@linux.dev/

Eduard Zingerman (3):
  selftests/bpf: update tcp_custom_syncookie to use scalar packet offset
  bpf: check bpf_func_state->callback_depth when pruning states
  selftests/bpf: test case for callback_depth states pruning logic

 kernel/bpf/verifier.c                         |  3 +
 .../bpf/progs/test_tcp_custom_syncookie.c     | 83 ++++++++++++-------
 .../bpf/progs/verifier_iterating_callbacks.c  | 70 ++++++++++++++++
 3 files changed, 126 insertions(+), 30 deletions(-)

-- 
2.43.0

[PATCH bpf-next 1/3] selftests/bpf: update tcp_custom_syncookie to use scalar packet offset

[Eduard Zingerman]

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 <eddyz87@gmail.com>
---
 .../bpf/progs/test_tcp_custom_syncookie.c     | 83 ++++++++++++-------
 1 file changed, 53 insertions(+), 30 deletions(-)

diff --git a/tools/testing/selftests/bpf/progs/test_tcp_custom_syncookie.c b/tools/testing/selftests/bpf/progs/test_tcp_custom_syncookie.c
index a5501b29979a..c8e4553648bf 100644
--- a/tools/testing/selftests/bpf/progs/test_tcp_custom_syncookie.c
+++ b/tools/testing/selftests/bpf/progs/test_tcp_custom_syncookie.c
@@ -10,6 +10,8 @@
 #include "test_siphash.h"
 #include "test_tcp_custom_syncookie.h"
 
+#define MAX_PACKET_OFF 0xffff
+
 /* Hash is calculated for each client and split into ISN and TS.
  *
  *       MSB                                   LSB
@@ -52,16 +54,15 @@ static siphash_key_t test_key_siphash = {
 
 struct tcp_syncookie {
 	struct __sk_buff *skb;
+	void *data;
 	void *data_end;
 	struct ethhdr *eth;
 	struct iphdr *ipv4;
 	struct ipv6hdr *ipv6;
 	struct tcphdr *tcp;
-	union {
-		char *ptr;
-		__be32 *ptr32;
-	};
+	__be32 *ptr32;
 	struct bpf_tcp_req_attrs attrs;
+	u32 off;
 	u32 cookie;
 	u64 first;
 };
@@ -70,6 +71,7 @@ bool handled_syn, handled_ack;
 
 static int tcp_load_headers(struct tcp_syncookie *ctx)
 {
+	ctx->data = (void *)(long)ctx->skb->data;
 	ctx->data_end = (void *)(long)ctx->skb->data_end;
 	ctx->eth = (struct ethhdr *)(long)ctx->skb->data;
 
@@ -134,6 +136,7 @@ static int tcp_reload_headers(struct tcp_syncookie *ctx)
 	if (bpf_skb_change_tail(ctx->skb, data_len + 60 - ctx->tcp->doff * 4, 0))
 		goto err;
 
+	ctx->data = (void *)(long)ctx->skb->data;
 	ctx->data_end = (void *)(long)ctx->skb->data_end;
 	ctx->eth = (struct ethhdr *)(long)ctx->skb->data;
 	if (ctx->ipv4) {
@@ -195,47 +198,68 @@ static int tcp_validate_header(struct tcp_syncookie *ctx)
 	return -1;
 }
 
-static int tcp_parse_option(__u32 index, struct tcp_syncookie *ctx)
+static __always_inline void *next(struct tcp_syncookie *ctx, __u32 sz)
 {
-	char opcode, opsize;
+	__u64 off = ctx->off;
+	__u8 *data;
 
-	if (ctx->ptr + 1 > ctx->data_end)
-		goto stop;
+	/* Verifier forbids access to packet when offset exceeds MAX_PACKET_OFF */
+	if (off > MAX_PACKET_OFF - sz)
+		return NULL;
+
+	data = ctx->data + off;
+	barrier_var(data);
+	if (data + sz >= ctx->data_end)
+		return NULL;
 
-	opcode = *ctx->ptr++;
+	ctx->off += sz;
+	return data;
+}
 
-	if (opcode == TCPOPT_EOL)
+static int tcp_parse_option(__u32 index, struct tcp_syncookie *ctx)
+{
+	__u8 *opcode, *opsize, *wscale;
+	__u32 *tsval, *tsecr;
+	__u16 *mss;
+	__u32 off;
+
+	off = ctx->off;
+	opcode = next(ctx, 1);
+	if (!opcode)
 		goto stop;
 
-	if (opcode == TCPOPT_NOP)
+	if (*opcode == TCPOPT_EOL)
+		goto stop;
+
+	if (*opcode == TCPOPT_NOP)
 		goto next;
 
-	if (ctx->ptr + 1 > ctx->data_end)
+	opsize = next(ctx, 1);
+	if (!opsize)
 		goto stop;
 
-	opsize = *ctx->ptr++;
-
-	if (opsize < 2)
+	if (*opsize < 2)
 		goto stop;
 
-	switch (opcode) {
+	switch (*opcode) {
 	case TCPOPT_MSS:
-		if (opsize == TCPOLEN_MSS && ctx->tcp->syn &&
-		    ctx->ptr + (TCPOLEN_MSS - 2) < ctx->data_end)
-			ctx->attrs.mss = get_unaligned_be16(ctx->ptr);
+		mss = next(ctx, 2);
+		if (*opsize == TCPOLEN_MSS && ctx->tcp->syn && mss)
+			ctx->attrs.mss = get_unaligned_be16(mss);
 		break;
 	case TCPOPT_WINDOW:
-		if (opsize == TCPOLEN_WINDOW && ctx->tcp->syn &&
-		    ctx->ptr + (TCPOLEN_WINDOW - 2) < ctx->data_end) {
+		wscale = next(ctx, 1);
+		if (*opsize == TCPOLEN_WINDOW && ctx->tcp->syn && wscale) {
 			ctx->attrs.wscale_ok = 1;
-			ctx->attrs.snd_wscale = *ctx->ptr;
+			ctx->attrs.snd_wscale = *wscale;
 		}
 		break;
 	case TCPOPT_TIMESTAMP:
-		if (opsize == TCPOLEN_TIMESTAMP &&
-		    ctx->ptr + (TCPOLEN_TIMESTAMP - 2) < ctx->data_end) {
-			ctx->attrs.rcv_tsval = get_unaligned_be32(ctx->ptr);
-			ctx->attrs.rcv_tsecr = get_unaligned_be32(ctx->ptr + 4);
+		tsval = next(ctx, 4);
+		tsecr = next(ctx, 4);
+		if (*opsize == TCPOLEN_TIMESTAMP && tsval && tsecr) {
+			ctx->attrs.rcv_tsval = get_unaligned_be32(tsval);
+			ctx->attrs.rcv_tsecr = get_unaligned_be32(tsecr);
 
 			if (ctx->tcp->syn && ctx->attrs.rcv_tsecr)
 				ctx->attrs.tstamp_ok = 0;
@@ -244,13 +268,12 @@ static int tcp_parse_option(__u32 index, struct tcp_syncookie *ctx)
 		}
 		break;
 	case TCPOPT_SACK_PERM:
-		if (opsize == TCPOLEN_SACK_PERM && ctx->tcp->syn &&
-		    ctx->ptr + (TCPOLEN_SACK_PERM - 2) < ctx->data_end)
+		if (*opsize == TCPOLEN_SACK_PERM && ctx->tcp->syn)
 			ctx->attrs.sack_ok = 1;
 		break;
 	}
 
-	ctx->ptr += opsize - 2;
+	ctx->off = off + *opsize;
 next:
 	return 0;
 stop:
@@ -259,7 +282,7 @@ static int tcp_parse_option(__u32 index, struct tcp_syncookie *ctx)
 
 static void tcp_parse_options(struct tcp_syncookie *ctx)
 {
-	ctx->ptr = (char *)(ctx->tcp + 1);
+	ctx->off = (__u8 *)(ctx->tcp + 1) - (__u8 *)ctx->data,
 
 	bpf_loop(40, tcp_parse_option, ctx, 0);
 }
-- 
2.43.0

[PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman]

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/9b251840-7cb8-4d17-bd23-1fc8071d8eef@linux.dev/

Suggested-by: Yonghong Song <yonghong.song@linux.dev>
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
---
 kernel/bpf/verifier.c | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index ddaf09db1175..df99fcdbaa05 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -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))
-- 
2.43.0

[PATCH bpf-next 3/3] selftests/bpf: test case for callback_depth states pruning logic

[Eduard Zingerman]

The test case was minimized from mailing list discussion [0].
It is equivalent to the following C program:

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

    static __naked void iter_limit_bug_cb(void)
    {
    	switch (bpf_get_prandom_u32()) {
    	case 1:  ctx->a = 42; break;
    	case 2:  ctx->b = 42; break;
    	default: ctx->c = 42; break;
    	}
    }

    int iter_limit_bug(struct __sk_buff *skb)
    {
    	struct iter_limit_bug_ctx ctx = { 7, 7, 7 };

    	bpf_loop(2, iter_limit_bug_cb, &ctx, 0);
    	if (ctx.a == 42 && ctx.b == 42 && ctx.c == 7)
    	  asm volatile("r1 /= 0;":::"r1");
    	return 0;
    }

The main idea is that each loop iteration changes one of the state
variables in a non-deterministic manner. Hence it is premature to
prune the states that have two iterations left comparing them to
states with one iteration left.
E.g. {{7,7,7}, callback_depth=0} can reach state {42,42,7},
while {{7,7,7}, callback_depth=1} can't.

[0] https://lore.kernel.org/bpf/9b251840-7cb8-4d17-bd23-1fc8071d8eef@linux.dev/

Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
---
 .../bpf/progs/verifier_iterating_callbacks.c  | 70 +++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_iterating_callbacks.c b/tools/testing/selftests/bpf/progs/verifier_iterating_callbacks.c
index 5905e036e0ea..a955a6358206 100644
--- a/tools/testing/selftests/bpf/progs/verifier_iterating_callbacks.c
+++ b/tools/testing/selftests/bpf/progs/verifier_iterating_callbacks.c
@@ -239,4 +239,74 @@ int bpf_loop_iter_limit_nested(void *unused)
 	return 1000 * a + b + c;
 }
 
+struct iter_limit_bug_ctx {
+	__u64 a;
+	__u64 b;
+	__u64 c;
+};
+
+static __naked void iter_limit_bug_cb(void)
+{
+	/* This is the same as C code below, but written
+	 * in assembly to control which branches are fall-through.
+	 *
+	 *   switch (bpf_get_prandom_u32()) {
+	 *   case 1:  ctx->a = 42; break;
+	 *   case 2:  ctx->b = 42; break;
+	 *   default: ctx->c = 42; break;
+	 *   }
+	 */
+	asm volatile (
+	"r9 = r2;"
+	"call %[bpf_get_prandom_u32];"
+	"r1 = r0;"
+	"r2 = 42;"
+	"r0 = 0;"
+	"if r1 == 0x1 goto 1f;"
+	"if r1 == 0x2 goto 2f;"
+	"*(u64 *)(r9 + 16) = r2;"
+	"exit;"
+	"1: *(u64 *)(r9 + 0) = r2;"
+	"exit;"
+	"2: *(u64 *)(r9 + 8) = r2;"
+	"exit;"
+	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all
+	);
+}
+
+SEC("tc")
+__failure
+__flag(BPF_F_TEST_STATE_FREQ)
+int iter_limit_bug(struct __sk_buff *skb)
+{
+	struct iter_limit_bug_ctx ctx = { 7, 7, 7 };
+
+	bpf_loop(2, iter_limit_bug_cb, &ctx, 0);
+
+	/* This is the same as C code below,
+	 * written in assembly to guarantee checks order.
+	 *
+	 *   if (ctx.a == 42 && ctx.b == 42 && ctx.c == 7)
+	 *     asm volatile("r1 /= 0;":::"r1");
+	 */
+	asm volatile (
+	"r1 = *(u64 *)%[ctx_a];"
+	"if r1 != 42 goto 1f;"
+	"r1 = *(u64 *)%[ctx_b];"
+	"if r1 != 42 goto 1f;"
+	"r1 = *(u64 *)%[ctx_c];"
+	"if r1 != 7 goto 1f;"
+	"r1 /= 0;"
+	"1:"
+	:
+	: [ctx_a]"m"(ctx.a),
+	  [ctx_b]"m"(ctx.b),
+	  [ctx_c]"m"(ctx.c)
+	: "r1"
+	);
+	return 0;
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.43.0

Re: [PATCH bpf-next 1/3] selftests/bpf: update tcp_custom_syncookie to use scalar packet offset

[Yonghong Song]

On 2/12/24 6:38 AM, Eduard Zingerman wrote:
> 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 <eddyz87@gmail.com>

Acked-by: Yonghong Song <yonghong.song@linux.dev>

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Yonghong Song]

On 2/12/24 6:38 AM, Eduard Zingerman wrote:
> 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;
>      }
>
The change LGTM. But the below description seems not very clear to me.

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

Why we have '7P' here?

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

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

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

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

>        - (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.

>      - (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}.

It would be good to specify which 'checkpoint #2' has callback_depth of 1.

> 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'?

> This commit makes disallows such premature pruning.

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.

>
> [0] https://lore.kernel.org/bpf/9b251840-7cb8-4d17-bd23-1fc8071d8eef@linux.dev/
>
> Suggested-by: Yonghong Song <yonghong.song@linux.dev>
> Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
> ---
>   kernel/bpf/verifier.c | 3 +++
>   1 file changed, 3 insertions(+)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index ddaf09db1175..df99fcdbaa05 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -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))

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman]

On Mon, 2024-02-12 at 17:20 -0800, Yonghong Song wrote:
[...]

Hi Yonghong,

Thank you for the feedback, I put updated description at the end of
the email, below are the answers to your questions.

> > - (0) {7P,7,7}
> 
> Why we have '7P' here?

Precision is propagated because of the check in the "-> to end" branch,
made it more clear in the updated description.

> >    - (3) {7P,7,7}
> 
> So here when (3) is hit, we have callback_depth  = 1, right?

Yes, made callback depth explicit.

> >      - (0) {7P,7,42} (checkpoint #1):
> 
> So for below (3)/(2)/(1) we have callback_depth = 2, right?

Yes.
 
> >        - (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.

Yes.

[...]

> > 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'?

Gave it a name.

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

Added.

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

    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 };

    	/* 0 */ bpf_loop(2, loop_cb, &ctx, 0);
    	if (/* 4 */ ctx.a == 42 && ctx.b == 42 && ctx.c == 7)
    		/* 5 */ asm volatile("r0 /= 0;":::"r0");
    	/* 6 */ return 0;
    }

Prior to this commit verifier built the following checkpoint tree for
this example:

 .------------------------------------- checkpoint / state name
 |    .-------------------------------- code point number
 |    |   .---------------------------- stack state {ctx.a,ctx.b,ctx.c}
 |    |   |        .------------------- callback depth in frame #0
 v    v   v        v
   - (0) {7P,7P,7},depth=0
     - (3) {7P,7,7},depth=1
(a)    - (0) {7P,7,42},depth=1
         - (3) {7P,7,42},depth=2
           - (0) {7P,7,42},depth=2      loop terminates because of depth limit
             - (4) {7P,7,42},depth=0    predicted false, ctx.a marked precise
             - (6) exit
         - (2) {7P,7,42},depth=2
           - (0) {7P,42,42},depth=2     loop terminates because of depth limit
             - (4) {7P,42,42},depth=0   predicted false, ctx.a marked precise
             - (6) exit
(b)      - (1) {7P,7P,42},depth=2
           - (0) {42P,7P,42},depth=2    loop terminates because of depth limit
             - (4) {42P,7P,42},depth=0  predicted false, ctx.{a,b} marked precise
             - (6) exit
     - (2) {7P,7,7},depth=1
       - (0) {7P,42,7},depth=1          considered safe, pruned using checkpoint (a)
(c)  - (1) {7,7,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
       - (0) {42P,7,7P},depth=1
         ...
         - (2) {42,7,7},depth=2
           - (0) {42,42,7},depth=2      loop terminates because of depth limit
             - (4) {42,42,7},depth=0    predicted true, ctx.{a,b,c} marked precise
               - (5) division by zero

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

Wdyt?

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman]

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

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Yonghong Song]

On 2/13/24 10:14 AM, Eduard Zingerman wrote:
> 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)

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.

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

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman]

On Wed, 2024-02-14 at 09:42 -0800, Yonghong Song wrote:

> >   .------------------------------------- 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)
> 
> 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}.

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

> Other than the above, the diagram LGTM.

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

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Yonghong Song]

On 2/16/24 6:27 AM, Eduard Zingerman wrote:
> On Wed, 2024-02-14 at 09:42 -0800, Yonghong Song wrote:
>
>>>    .------------------------------------- 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)
>> 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}.

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.
With this flag,
   (c)  - (1) {7P,7P,7},depth=1            considered safe, pruned using checkpoint (b)
is correct.

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?
   

>
>> 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.
>
>> Other than the above, the diagram LGTM.
> Thank you for the feedback, I'll post v2 shortly.

Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman]

On Mon, 2024-02-19 at 16:25 -0800, Yonghong Song wrote:
> On 2/16/24 6:27 AM, Eduard Zingerman wrote:
> > On Wed, 2024-02-14 at 09:42 -0800, Yonghong Song wrote:
> > 
> > > >    .------------------------------------- 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)
> > > 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}.
> 
> 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.

Will do.

[...]

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

I think you are correct.