Re: [PATCH bpf-next v3 05/45] bpf: Add join of verifier states

[sashiko-bot@kernel.org]

Thank you for your contribution! Sashiko AI review found 3 potential issue(s) to consider:
- [Medium] bpf: asymmetric unallocated and poisoned stack handling in join_func()
- [Medium] bpf: join_reg() zeroing dst->delta breaks explore_alu_limits in join_check()
- [Medium] bpf: asymmetric out_stack_arg_cnt check in join_func() blocks valid joins
--

commit 1d1d176d0db968688ddcdf9cb26ad2c24d9339f4
Author: Alexei Starovoitov <ast@kernel.org>

bpf: Add join of verifier states

This commit adds the second half of kernel/bpf/join.c and enables building it.
It implements bpf_states_join() to merge two verifier states frame by frame at
a single instruction and verifies that the joined state subsumes both inputs.

> diff --git a/kernel/bpf/join.c b/kernel/bpf/join.c
> index fe513b7a8e884..4da051767e1d9 100644
> --- a/kernel/bpf/join.c
> +++ b/kernel/bpf/join.c
> @@ -398,3 +398,250 @@ static bool join_slot(struct bpf_join_state *js, struct bpf_stack_state *ds,
>  	bpf_mark_reg_not_init(js->env, &ds->spilled_ptr);
>  	return true;
>  }
> +

[ ... ]

> +static bool join_func(struct bpf_join_state *js, struct bpf_func_state *fd,
> +		      const struct bpf_func_state *fa, const struct bpf_func_state *fb,
> +		      u16 live_regs, int pass)
> +{

[ ... ]

> +	nslots_b = bpf_stack_nr_slots(fb);
> +	for (i = 0; i < bpf_stack_nr_slots(fa); i++) {
> +		const struct bpf_stack_state *sb = i < nslots_b ? bpf_stack_slot(fb, i) : NULL;
> +
> +		js->place = MAX_BPF_REG + i;
> +		if (!join_slot(js, bpf_stack_slot(fd, i), bpf_stack_slot(fa, i), sb, pass))
> +			return false;
> +	}
> +	js->place = -1;
> +	/* Slots that exist only in 'b' are STACK_INVALID in the result. */
> +	for (i = bpf_stack_nr_slots(fa); pass == 1 && i < nslots_b; i++) {
> +		const struct bpf_stack_state *sb = bpf_stack_slot(fb, i);
> +
> +		if (slot_is_special(sb) ||
> +		    (slot_has_spill(sb) && sb->spilled_ptr.type != SCALAR_VALUE))
> +			return false;
> +	}

[Severity: Medium]
As reported by Sashiko on v2 [1], how does bpf_states_join() -> join_func() ->
join_slot() handle stack slots when !env->allow_uninit_stack?

First, in the loop over slots that exist only in fb (for i >=
bpf_stack_nr_slots(fa)), join_func() only rejects special slots and non-scalar
spills, without checking !js->env->allow_uninit_stack. If fb has a live
initialized slot at i >= bpf_stack_nr_slots(fa) (such as a scalar STACK_SPILL,
STACK_MISC, or STACK_ZERO) while fa has allocated_stack <= i * 8, the join
succeeds and leaves slot i unallocated in fd. If the program later reads slot
i under a condition that only holds along path b, won't
check_stack_slot_within_bounds() falsely reject a valid program with -EACCES
when !env->allow_uninit_stack?

Second, when bpf_clean_verifier_state() marks dead stack slots in fa as
STACK_POISON via __clean_func_state(), and slot i is unallocated in fb (so
join_slot() substitutes invalid_slot with STACK_INVALID), join_slot() runs:

	if (!js->env->allow_uninit_stack)
		return !memcmp(sa->slot_type, sb->slot_type, sizeof(sa->slot_type));

Won't memcmp() treat dead STACK_POISON bytes in sa and unallocated
STACK_INVALID bytes in sb as unequal, causing dead stack slots to prevent a
join when !env->allow_uninit_stack?

> +
> +	if (fa->out_stack_arg_cnt < fb->out_stack_arg_cnt)
> +		return false;

[Severity: Medium]
As reported by Sashiko on v2 [2], should join_func() reject the join whenever
fa->out_stack_arg_cnt < fb->out_stack_arg_cnt?

Since out_stack_arg_cnt is an allocation high-water mark grown by
grow_stack_arg_slots() in check_stack_arg_write(), it is not reset to 0 when
invalidate_outgoing_stack_args() or bpf_flow_return() marks
stack_arg_regs[0..out_stack_arg_cnt - 1] as NOT_INIT after a call returns.

If state a reaches a loop header or branch target before any call with stack
arguments (fa->out_stack_arg_cnt == 0) and state b arrives after a call with
stack arguments whose slots are now NOT_INIT (fb->out_stack_arg_cnt > 0),
won't this check prevent joining or widening the states even though slots at
i >= fa->out_stack_arg_cnt are implicitly NOT_INIT in fa and fd?

[ ... ]

> +/* The result has to describe everything that an input describes */
> +static int join_check(struct bpf_join_state *js, struct bpf_verifier_state *dst,
> +		      const struct bpf_verifier_state *in, const char *which)
> +{
> +	struct bpf_verifier_env *env = js->env;
> +
> +	if (bpf_state_subsumes(env, dst, (struct bpf_verifier_state *)in))
> +		return 0;
> +	/* check_ids() has no room left: that says nothing about the join */
> +	if (env->idmap_scratch.cnt == BPF_ID_MAP_SIZE)
> +		return 1;
> +	bpf_log(&env->log, "join:");
> +	print_verifier_state(env, dst, dst->curframe, true);
> +	bpf_log(&env->log, "input %s:", which);
> +	print_verifier_state(env, in, in->curframe, true);
> +	verifier_bug(env, "join of states at insn %u does not subsume input '%s'",
> +		     dst->insn_idx, which);
> +	return -EFAULT;
> +}

[Severity: Medium]
As reported by Sashiko on v2 [3], can bpf_states_join() trigger verifier_bug()
in join_check() when env->explore_alu_limits is true?

In join_reg() for SCALAR_VALUE:

	case SCALAR_VALUE:
		if (js->env->explore_alu_limits && !reg_value_equal(ra, rb))
			return false;
		if (pass == 1) {
			jid_note(js, ra->id, rb->id, scalar_link_consistent(ra, rb));
			return true;
		}
		join_range(js, dst, ra, rb);
		/* a link that exists on one side only is dropped */
		if (ra->id && !jid_good(js, ra->id, rb->id)) {
			dst->id = 0;
			dst->delta = 0;
		}
		return true;

Two SCALAR_VALUE registers ra and rb with equal ranges and the same non-zero
delta pass reg_value_equal(ra, rb). If their IDs do not form a valid bijection
across the state (so jid_good(js, ra->id, rb->id) is false in pass 2),
join_reg() clears dst->id = 0 and dst->delta = 0.

When join_check() subsequently calls bpf_state_subsumes() -> states_equal() ->
func_states_equal() -> regsafe(), regsafe() checks:

	if (env->explore_alu_limits) {
		return memcmp(rold, rcur, offsetof(struct bpf_reg_state, id)) == 0 &&
		       check_scalar_ids(rold->id, rcur->id, idmap);
	}

Because delta lies before id in struct bpf_reg_state, won't memcmp() fail when
comparing dst->delta (0) against ra->delta (non-zero), causing join_check() to
hit verifier_bug() and return -EFAULT?

[1] https://lore.kernel.org/r/20261105204513.2230344-6-alexei.starovoitov@gmail.com
[2] https://lore.kernel.org/r/20261105204513.2230344-6-alexei.starovoitov@gmail.com
[3] https://lore.kernel.org/r/20261105204513.2230344-6-alexei.starovoitov@gmail.com

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/20261106035111.3315285-1-alexei.starovoitov@gmail.com?part=5