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

[Yonghong Song <yonghong.song@linux.dev>]

On 2/22/24 7:41 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] (assume that BPF_F_TEST_STATE_FREQ is set).
> 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:
>
>   .------------------------------------- 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,7P,7},depth=1
>         - (0) {7P,7P,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
> (a)      - (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             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
>         - (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
>
> [0] https://lore.kernel.org/bpf/9b251840-7cb8-4d17-bd23-1fc8071d8eef@linux.dev/
>
> Fixes: bb124da69c47 ("bpf: keep track of max number of bpf_loop callback iterations")
> Suggested-by: Yonghong Song <yonghong.song@linux.dev>
> Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>

Thanks for updating commit messages. It looks correct to me.

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