Re: [PATCH bpf-next v4 05/46] bpf: Add join of verifier states

[sashiko-bot@kernel.org]

Thank you for your contribution! Sashiko AI review found 2 potential
issues to consider:
- [Medium] bpf: join_reg() zeroing dst->delta breaks explore_alu_limits
  in join_check()
- [Medium] bpf: asymmetric unallocated and poisoned stack handling in
  join_func()
--

commit 81dc6f947daf4ec051f2b11325ec95b20b615ab2
Author: Alexei Starovoitov <ast@kernel.org>

bpf: Add join of verifier states

This commit completes the state-joining implementation in join.c by adding
frame, reference, loop stack, and whole-state join logic along with a
subsumption check on the resulting state.

> 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;
>  }

[ ... ]

> +	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]
When !js->env->allow_uninit_stack, does this loop drop live initialized
stack slots that exist only in fb?

For slots beyond bpf_stack_nr_slots(fa), the loop only rejects special
slots and non-scalar spills.  If fb has a live scalar STACK_SPILL,
STACK_MISC, or STACK_ZERO slot at i >= bpf_stack_nr_slots(fa), the join
succeeds (since stacksafe() only checks up to fd->allocated_stack, which is
copied from fa) and leaves slot i unallocated in fd, causing later reads on
path b to fail verification with -EACCES.  When fa and fb are passed in the
opposite order, join_slot() rejects the join at:

kernel/bpf/join.c:join_slot() {
	...
	/* the prog can't read uninitialized stack: slots of different kinds have no join */
	if (!js->env->allow_uninit_stack)
		return !memcmp(sa->slot_type, sb->slot_type, sizeof(sa->slot_type));
}

Conversely, when bpf_stack_nr_slots(fa) > bpf_stack_nr_slots(fb) and
bpf_clean_verifier_state() has marked dead slots in fa as STACK_POISON,
join_slot() substitutes invalid_slot (all STACK_INVALID) for the missing
slot in fb, and the memcmp() above rejects the join because STACK_POISON !=
STACK_INVALID, even though both represent dead/unallocated stack bytes.

[ ... ]

> +/* 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]
Can join_check() trigger a false verifier_bug() when env->explore_alu_limits
is set and join_reg() drops an inconsistent scalar link?

In struct bpf_reg_state, delta lies before id.  In join_reg(), two
SCALAR_VALUE registers with matching non-zero delta and identical ranges
pass reg_value_equal(ra, rb) when js->env->explore_alu_limits is true, but
if their IDs do not form a consistent bijection across the states, pass 2
clears both dst->id and dst->delta:

kernel/bpf/join.c:join_reg() {
	...
	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;
}

When join_check() then calls bpf_state_subsumes(), regsafe() checks:

kernel/bpf/states.c:regsafe() {
	...
	case SCALAR_VALUE:
		if (env->explore_alu_limits) {
			/* explore_alu_limits disables tnum_in() and range_within()
			 * logic and requires everything to be strict
			 */
			return memcmp(rold, rcur, offsetof(struct bpf_reg_state, id)) == 0 &&
			       check_scalar_ids(rold->id, rcur->id, idmap);
		}
}

Because dst->delta is now 0 while the input register still has a non-zero
delta, memcmp() fails and join_check() hits verifier_bug() and returns
-EFAULT.

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