Re: [PATCH v2 bpf-next 13/18] bpf: Check the return values of fmod_ret programs on found targets

[bot+bpf-ci@kernel.org]

[-- Attachment #1: Type: text/plain, Size: 3043 bytes --]

> bpf: Check the return values of fmod_ret programs on found targets

TL;DR: The fmod_ret return check may wrongly reject valid programs: when
states returning two allowed constants merge at a shared exit, R0 becomes a
range, not a constant, and the load fails.

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c

[ ... ]

> +/* The program must return a constant: 0 or one of the values of the tag */
> +static int check_fmodret_retval(struct bpf_verifier_env *env, int regno,
> +				const char *exit_ctx, const char *reg_name)
> +{
> +	const struct bpf_prog_aux *aux = env->prog->aux;
> +	struct bpf_reg_state *reg = reg_state(env, regno);
> +	u32 i;
> +
> +	if (reg->type == SCALAR_VALUE && tnum_is_const(reg->var_off) &&
> +	    fmodret_retval_allowed(aux, reg->var_off.value))
> +		return 0;

Can this reject valid programs when two allowed constants are joined at a
shared exit?

The main pass is the fixpoint in kernel/bpf/flow.c, and flow_merge() joins
states that reach the same basic-block head.  For SCALAR_VALUE, join_reg()
-> join_range() produces the union range.  flow_join_makes_up() only
refuses the join when flow_gap() finds values in the union that neither
state has, and only while flow_has_room().  The FLOW_NEED_ARG table has no
entry for R0 at BPF_EXIT, so flow_needed_consts_differ() does not keep the
constants apart.

For a target tagged "bpf_fmodret_retval:-12,-11":

  r2 = *(u64 *)(r1 + 0)
  r0 = -11
  if r2 == 0 goto +1
  r0 = -12
  exit

The states at exit (R0=-11 and R0=-12) are disjoint but leave no gap, so
they become R0=[-12,-11] and tnum_is_const() fails.  The load then fails
with:

  At program exit the register R0 must be a constant, it should be 0 or
  one of -12,-11

even though every path returns an allowed value.

The same can happen with the common pattern "r0 = 0 ... r0 = -1; exit" when
the tag contains -1, since the 64-bit constants 0 and 0xffffffffffffffff
touch on the circle and are joined.  Once a program uses half of the state
limits, flow_has_room() is false and even gapped values such as -34 and -22
are joined.

The selftest join_both_paths avoids this only by using two separate exit
instructions, and whether exits are merged is the compiler's choice.

Every other exit check so far was a range check via retval_range_within(),
but this one needs set membership.  Should R0 at the main-prog exit (and R1
at bpf_throw without a callback) be added to the FLOW_NEED_ARG table for
programs with fmodret_retvals, or should a small bounded range be accepted
when every value in it is 0 or in the list?

The feature becomes reachable once 1c163e52401e ("resolve_btfids: Tag
fmod_ret candidates as targets") emits the tags, and no later commit in the
series changes this.


---
AI reviewed your patch. Please fix the bug or email reply why it's not a bug.
See: https://github.com/kernel-patches/vmtest/blob/master/ci/claude/README.md

CI run summary: https://github.com/kernel-patches/bpf/actions/runs/42662799554