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

[Eduard Zingerman <eddyz87@gmail.com>]

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?