Re: [PATCH bpf-next v5 15/25] bpf: Teach verifier about non-size constant arguments

[Andrii Nakryiko <andrii.nakryiko@gmail.com>]

On Mon, Nov 7, 2022 at 3:10 PM Kumar Kartikeya Dwivedi <memxor@gmail.com> wrote:
>
> Currently, the verifier has support for various arguments that either
> describe the size of the memory being passed in to a helper, or describe
> the size of the memory being returned. When a constant is passed in like
> this, it is assumed for the purposes of precision tracking that if the
> value in the already explored safe state is within the value in current
> state, it would fine to prune the search.
>
> While this holds well for size arguments, arguments where each value may
> denote a distinct meaning and needs to be verified separately needs more
> work. Search can only be pruned if both are equivalent values. In all
> other cases, it would be incorrect to treat those two precise registers
> as equivalent if the new value satisfies the old one (i.e. old <= cur).
>
> Hence, make the register precision marker tri-state. There are now three
> values that reg->precise takes: NOT_PRECISE, PRECISE, EXACT.
>
> Both PRECISE and EXACT are 'true' values. EXACT affects how regsafe
> decides whether both registers are equivalent for the purposes of
> verifier state equivalence. When it sees that old state register has
> reg->precise == EXACT, unless both are equivalent, it will return false.
> Otherwise, for PRECISE case it falls back to the default check that is
> present now (i.e. thinking that we're talking about sizes).
>
> This is required as a future patch introduces a BPF memory allocator
> interface, where we take the program BTF's type ID as an argument. Each
> distinct type ID may result in the returned pointer obtaining a
> different size, hence precision tracking is needed, and pruning cannot
> just happen when the old value is within the current value. It must only
> happen when the type ID is equal. The type ID will always correspond to
> prog->aux->btf hence actual type match is not required.
>
> Finally, change mark_chain_precision precision argument to EXACT for
> kfuncs constant non-size scalar arguments (tagged with __k suffix).
>
> Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
> ---

I think this needs a bit more thinking, tbh. First, with my recent
changes we don't even set precision marks in current state, everything
stays imprecise. And then under CAP_BPF we also aggressively reset
precision. This might work for EXACT, but needs careful consideration.

But, taking a step back. I'm trying to understand why this whole EXACT
mode is necessary. SCALAR has min/max values which regsafe() does
check. So for those special ___k arguments, if we correctly set
min/max values to be *exactly* the btf_id passed in, why would
regsafe()'s logic not work?

>  include/linux/bpf_verifier.h |  10 +++-
>  kernel/bpf/verifier.c        | 111 ++++++++++++++++++++++-------------
>  2 files changed, 76 insertions(+), 45 deletions(-)
>
> diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
> index f3a601d33fb3..1e246ec2ff37 100644
> --- a/include/linux/bpf_verifier.h
> +++ b/include/linux/bpf_verifier.h
> @@ -43,6 +43,12 @@ enum bpf_reg_liveness {
>         REG_LIVE_DONE = 0x8, /* liveness won't be updating this register anymore */
>  };
>
> +enum bpf_reg_precise {
> +       NOT_PRECISE,

IMPRECISE?

> +       PRECISE,
> +       EXACT,
> +};
> +
>  struct bpf_reg_state {
>         /* Ordering of fields matters.  See states_equal() */
>         enum bpf_reg_type type;
> @@ -180,7 +186,7 @@ struct bpf_reg_state {
>         s32 subreg_def;
>         enum bpf_reg_liveness live;
>         /* if (!precise && SCALAR_VALUE) min/max/tnum don't affect safety */
> -       bool precise;
> +       enum bpf_reg_precise precise;
>  };
>
>  enum bpf_stack_slot_type {
> @@ -626,8 +632,6 @@ int bpf_check_attach_target(struct bpf_verifier_log *log,
>                             struct bpf_attach_target_info *tgt_info);
>  void bpf_free_kfunc_btf_tab(struct bpf_kfunc_btf_tab *tab);
>
> -int mark_chain_precision(struct bpf_verifier_env *env, int regno);
> -
>  #define BPF_BASE_TYPE_MASK     GENMASK(BPF_BASE_TYPE_BITS - 1, 0)
>
>  /* extract base type from bpf_{arg, return, reg}_type. */
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 7515b31d2c40..5bfc151711b9 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -864,7 +864,7 @@ static void print_verifier_state(struct bpf_verifier_env *env,
>                 print_liveness(env, reg->live);
>                 verbose(env, "=");
>                 if (t == SCALAR_VALUE && reg->precise)
> -                       verbose(env, "P");
> +                       verbose(env, reg->precise == EXACT ? "E" : "P");
>                 if ((t == SCALAR_VALUE || t == PTR_TO_STACK) &&
>                     tnum_is_const(reg->var_off)) {
>                         /* reg->off should be 0 for SCALAR_VALUE */
> @@ -961,7 +961,7 @@ static void print_verifier_state(struct bpf_verifier_env *env,
>                         t = reg->type;
>                         verbose(env, "=%s", t == SCALAR_VALUE ? "" : reg_type_str(env, t));
>                         if (t == SCALAR_VALUE && reg->precise)
> -                               verbose(env, "P");
> +                               verbose(env, reg->precise == EXACT ? "E" : "P");
>                         if (t == SCALAR_VALUE && tnum_is_const(reg->var_off))
>                                 verbose(env, "%lld", reg->var_off.value + reg->off);
>                 } else {
> @@ -1695,7 +1695,16 @@ static void __mark_reg_unknown(const struct bpf_verifier_env *env,
>         reg->type = SCALAR_VALUE;
>         reg->var_off = tnum_unknown;
>         reg->frameno = 0;
> -       reg->precise = !env->bpf_capable;
> +       /* Helpers requiring EXACT for constant arguments cannot be called from
> +        * programs without CAP_BPF. This is because we don't propagate
> +        * precision markers when CAP_BPF is missing. If we allowed calling such
> +        * heleprs in those programs, the default would have to be EXACT for
> +        * them, which would be too aggresive, or we'd have to propagate it.

typos: helpers, aggressive

> +        *
> +        * Currently, only bpf_obj_new kfunc requires EXACT precision for its
> +        * scalar argument, which is a kfunc (and thus behind CAP_BPF).
> +        */
> +       reg->precise = !env->bpf_capable ? PRECISE : NOT_PRECISE;
>         __mark_reg_unbounded(reg);
>  }
>

[...]

>         /* Do sanity checks against current state of register and/or stack
>          * slot, but don't set precise flag in current state, as precision
> @@ -2969,7 +2982,7 @@ static int __mark_chain_precision(struct bpf_verifier_env *env, int frame, int r
>                                                 reg_mask &= ~(1u << i);
>                                                 continue;
>                                         }
> -                                       reg->precise = true;
> +                                       reg->precise = precise;
>                                 }
>                                 return 0;
>                         }
> @@ -2988,7 +3001,7 @@ static int __mark_chain_precision(struct bpf_verifier_env *env, int frame, int r
>                                 err = backtrack_insn(env, i, &reg_mask, &stack_mask);
>                         }
>                         if (err == -ENOTSUPP) {
> -                               mark_all_scalars_precise(env, st);
> +                               mark_all_scalars_precise(env, st, precise);

well... do you really intend to remark everything as EXACT, even
registers that have no business of being EXACT? Seems a bit too blunt.

>                                 return 0;
>                         } else if (err) {
>                                 return err;
> @@ -3029,7 +3042,7 @@ static int __mark_chain_precision(struct bpf_verifier_env *env, int frame, int r
>                         }
>                         if (!reg->precise)
>                                 new_marks = true;
> -                       reg->precise = true;
> +                       reg->precise = precise;
>                 }
>
>                 bitmap_from_u64(mask, stack_mask);

[...]