Re: [PATCH bpf-next v2 05/35] 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: join_reg() zeroing dst->delta breaks explore_alu_limits in join_check()
- [Medium] bpf: asymmetric unallocated and poisoned stack handling in join_func()
- [Medium] bpf: asymmetric out_stack_arg_cnt check in join_func() blocks valid joins
--

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

bpf: Add join of verifier states

This commit adds the second half of kernel/bpf/join.c and builds it to
implement bpf_states_join(), which joins two BPF verifier states frame by
frame at an 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]
When !js->env->allow_uninit_stack (for programs loaded without CAP_PERFMON),
can this stack slot handling in join_func() and join_slot() cause asymmetric
behavior depending on which state has the larger allocated_stack?

First, when bpf_stack_nr_slots(fa) < bpf_stack_nr_slots(fb), the loop over
slots i in [bpf_stack_nr_slots(fa), nslots_b) only rejects special slots and
non-scalar spills:

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

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 not allocated
that slot, bpf_states_join() succeeds and leaves slot i unallocated in fd.
If a later path predicated on the branch that came from fb reads fp - (i + 1)
* 8, check_stack_slot_within_bounds() will reject the valid program with
-EACCES because fd->allocated_stack is too small and !env->allow_uninit_stack.

Second, when bpf_stack_nr_slots(fa) > bpf_stack_nr_slots(fb),
bpf_clean_verifier_state() marks dead stack slots in fa as STACK_POISON
without growing fb->allocated_stack. For i >= nslots_b, join_func() passes
sb = NULL into join_slot(), which substitutes invalid_slot (all
STACK_INVALID) and checks:

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

Because memcmp() treats STACK_POISON in sa and STACK_INVALID in invalid_slot
as unequal, dead stack slots in fa prevent joining the two states.

Should join_slot() treat stype_is_invalid() bytes (STACK_INVALID and
STACK_POISON) as equivalent when !js->env->allow_uninit_stack, and should the
trailing loop in join_func() also reject non-invalid slots in fb when
!js->env->allow_uninit_stack?

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

[Severity: Medium]
Why does join_func() reject the join when fa->out_stack_arg_cnt <
fb->out_stack_arg_cnt?

In check_stack_arg_write(), grow_stack_arg_slots() grows out_stack_arg_cnt as
a high-water mark, and invalidate_outgoing_stack_args() or bpf_flow_return()
marks stack_arg_regs[0..out_stack_arg_cnt - 1] as NOT_INIT after a call
without resetting out_stack_arg_cnt to 0.

If state a reaches a loop header or join point before any call with stack
arguments (fa->out_stack_arg_cnt == 0) and state b arrives after calling a
function with stack arguments (fb->out_stack_arg_cnt > 0, with all slots
NOT_INIT), fa->out_stack_arg_cnt < fb->out_stack_arg_cnt prevents joining or
widening the two states.

Since slots beyond fa->out_stack_arg_cnt are implicitly NOT_INIT in both fa
and fd (and stack_arg_safe() in bpf_state_subsumes() already accepts that),
could join_func() allow fa->out_stack_arg_cnt < fb->out_stack_arg_cnt when
the extra slots in fb are NOT_INIT or incoming?

[ ... ]
> +/* 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() and return -EFAULT when
env->explore_alu_limits is enabled and join_reg() drops an inconsistent
scalar ID link?

In 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 env->explore_alu_limits is true and two SCALAR_VALUE registers ra and rb
have identical value ranges and the same non-zero delta (from BPF_ADD_CONST64
or BPF_ADD_CONST32), reg_value_equal(ra, rb) succeeds because memcmp(ra, rb,
offsetof(struct bpf_reg_state, id)) is 0.

If their IDs do not form a valid bijection across the state, jid_good(js,
ra->id, rb->id) returns false in pass 2, and join_reg() sets dst->id = 0 and
dst->delta = 0.

However, delta is located before id in struct bpf_reg_state. When
bpf_states_join() then calls join_check() -> bpf_state_subsumes() ->
states_equal() -> func_states_equal() -> regsafe(), regsafe() checks:

	case SCALAR_VALUE:
		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 rold->delta (dst->delta == 0) no longer matches rcur->delta
(ra->delta != 0), memcmp() fails, causing join_check() to fire verifier_bug()
and fail verification with -EFAULT.

Should join_reg() return false in pass 2 when js->env->explore_alu_limits is
set and dst->delta would be cleared alongside dst->id?

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