Re: [PATCH bpf-next v2 14/43] bpf: representation for intervals with steps

[sashiko-bot@kernel.org]

Thank you for your contribution! Sashiko AI review found 1 potential issue(s) to consider:
- [High] bpf: unsound scalar pruning in explore_alu_limits due to ignored stride
--

commit d4d6630f513d526c40cb9f5ea524c5bd6dd31948
Author: Eduard Zingerman <eddyz87@gmail.com>

bpf: representation for intervals with steps

Extends scalar register tracking with base and step fields to represent
strided values (base + step * k). Updates verifier ALU operations to
propagate these bounds.

> diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
> index 4371fb3405acb..05914fcbe77cd 100644
> --- a/include/linux/bpf_verifier.h
> +++ b/include/linux/bpf_verifier.h
> @@ -178,6 +178,13 @@ struct bpf_reg_state {
>  	 * during state comparisons.
>  	 */
>  	u32 map_uid;
> +	/*
> +	 * The value described by this register, interpreted as s64, lies on
> +	 * a line described by a linear equation base + step * k.
> +	 * Invariant: base < step.
> +	 */
> +	u16 base;
> +	u16 step;

[Severity: High]
Does adding these fields after the id field bypass the exact state comparison
checks?

Functions like regs_exact() and scalars_exact_for_widen() use
offsetof(struct bpf_reg_state, id) for their memcmp() limit. Because
base and step are positioned after id in the struct, they are excluded from
the memcmp().

For example, in kernel/bpf/states.c:regsafe():

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

When explore_alu_limits is enabled, could the verifier incorrectly prune
an unsafe execution branch (e.g. one with an unaligned scalar step) using
a cached safe branch that had an aligned step? This might allow unaligned
scalar offsets to bypass BTF array bounds alignment checks.

A similar omission occurs in regs_exact() which could cause false-positive
infinite loop detections, and in scalars_exact_for_widen() which might break
loop convergence expectations. Should these exact-match functions be updated
to explicitly compare the base and step fields?

>  	/* if (!precise && SCALAR_VALUE) min/max/tnum don't affect safety */
>  	bool precise;
>  };

-- 
Sashiko AI review · https://sashiko.dev/#/patchset/20261004-scev-minimal-rebase-v2-0-f6254e29fdf2@gmail.com?part=14