Message ID | 20231121002221.3687787-9-andrii@kernel.org (mailing list archive) |
---|---|
State | Superseded |
Delegated to: | BPF |
Headers | show |
Series | Complete BPF verifier precision tracking support for register spills | expand |
On Mon, Nov 20, 2023 at 04:22:19PM -0800, Andrii Nakryiko wrote: > include it here. But the reduction in states is due to the following > piece of C code: > > unsigned long ino; > > ... > > sk = s->sk_socket; > if (!sk) { > ino = 0; > } else { > inode = SOCK_INODE(sk); > bpf_probe_read_kernel(&ino, sizeof(ino), &inode->i_ino); > } > BPF_SEQ_PRINTF(seq, "%-8u %-8lu\n", s->sk_drops.counter, ino); > return 0; > > You can see that in some situations `ino` is zero-initialized, while in > others it's unknown value filled out by bpf_probe_read_kernel(). Before > this change both branches have to be validated twice. Once with I think you wanted to say that the code _after_ both branches converge had to be validated twice. With or without this patch both branches (ino = 0 and probe_read) will be validated only once. It's the code that after the branch that gets state pruned after this patch. > (precise) ino == 0, due to eager STACK_ZERO logic, and then again for > when ino is just STACK_MISC. But BPF_SEQ_PRINTF() doesn't care about > precise value of ino, so with the change in this patch verifier is able > to prune states from one of the branches, reducing number of total > states (and instructions) required for successful validation. This part is good.
On Tue, Nov 21, 2023 at 12:38 PM Alexei Starovoitov <alexei.starovoitov@gmail.com> wrote: > > On Mon, Nov 20, 2023 at 04:22:19PM -0800, Andrii Nakryiko wrote: > > include it here. But the reduction in states is due to the following > > piece of C code: > > > > unsigned long ino; > > > > ... > > > > sk = s->sk_socket; > > if (!sk) { > > ino = 0; > > } else { > > inode = SOCK_INODE(sk); > > bpf_probe_read_kernel(&ino, sizeof(ino), &inode->i_ino); > > } > > BPF_SEQ_PRINTF(seq, "%-8u %-8lu\n", s->sk_drops.counter, ino); > > return 0; > > > > You can see that in some situations `ino` is zero-initialized, while in > > others it's unknown value filled out by bpf_probe_read_kernel(). Before > > this change both branches have to be validated twice. Once with > > I think you wanted to say that the code _after_ both branches converge > had to be validated twice. > With or without this patch both branches (ino = 0 and probe_read) > will be validated only once. It's the code that after the branch > that gets state pruned after this patch. Yes, correct, it's the common code after two branches that now will converge, so BPF_SEQ_PRINTF() invocation in this case, I'll improve the wording. In practice a slightly modified variant also happens: we zero-initialize something, then depending on some conditions (error checking, etc), we overwrite zero-initialized stack slots with some unknown values that are not precise. Before this change we'll have STACK_ZERO and STACK_MISC in different branches/code paths, which would effectively duplicate all subsequent states that needs to be verified. Now there is a high chance for this STACK_ZERO vs STACK_MISC to not matter at all. We also can have spilled imprecise SCALAR_VALUE register instead of STACK_MISC. The principal idea is that STACK_ZERO promises a lot (that it is precisely zero), while often time those values are just some integers with values we don't care about. > > > (precise) ino == 0, due to eager STACK_ZERO logic, and then again for > > when ino is just STACK_MISC. But BPF_SEQ_PRINTF() doesn't care about > > precise value of ino, so with the change in this patch verifier is able > > to prune states from one of the branches, reducing number of total > > states (and instructions) required for successful validation. > > This part is good.
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index 00e6b17b71d0..ddb0888e7453 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -4405,8 +4405,7 @@ static int check_stack_write_fixed_off(struct bpf_verifier_env *env, return err; mark_stack_slot_scratched(env, spi); - if (reg && !(off % BPF_REG_SIZE) && register_is_bounded(reg) && - !register_is_null(reg) && env->bpf_capable) { + if (reg && !(off % BPF_REG_SIZE) && register_is_bounded(reg) && env->bpf_capable) { save_register_state(env, state, spi, reg, size); /* Break the relation on a narrowing spill. */ if (fls64(reg->umax_value) > BITS_PER_BYTE * size) @@ -4455,7 +4454,12 @@ static int check_stack_write_fixed_off(struct bpf_verifier_env *env, /* when we zero initialize stack slots mark them as such */ if ((reg && register_is_null(reg)) || (!reg && is_bpf_st_mem(insn) && insn->imm == 0)) { - /* backtracking doesn't work for STACK_ZERO yet. */ + /* STACK_ZERO case happened because register spill + * wasn't properly aligned at the stack slot boundary, + * so it's not a register spill anymore; force + * originating register to be precise to make + * STACK_ZERO correct for subsequent states + */ err = mark_chain_precision(env, value_regno); if (err) return err;