| Message ID | 20240212143832.28838-3-eddyz87@gmail.com (mailing list archive) |
|---|---|
| State | Superseded |
| Delegated to: | BPF |
| Headers | show |
| Series | check bpf_func_state->callback_depth when pruning states | expand |
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))
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?
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 ---
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 ---
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.
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.
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.
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))
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(+)