Re: [PATCH bpf v1 1/2] bpf: Fix state pruning check for PTR_TO_MAP_VALUE

[sdf@google.com]

On 11/12, Kumar Kartikeya Dwivedi wrote:
> Currently, the verifier preserves reg->id for PTR_TO_MAP_VALUE when it
> points to a map value that contains a bpf_spin_lock element (see the
> logic in reg_may_point_to_spin_lock and how it is used to skip setting
> reg->id to 0 in mark_ptr_or_null_reg). This gives a unique lock ID for
> each critical section begun by a bpf_spin_lock helper call.

> The same reg->id is matched with env->active_spin_lock during unlock to
> determine whether bpf_spin_unlock is called for the same bpf_spin_lock
> object.

> However, regsafe takes a different approach to safety checks currently.
> The comparison of reg->id was explicitly skipped in the commit being
> fixed with the reasoning that the reg->id value should have no bearing
> on the safety of the program if the old state was verified to be safe.

> This however is demonstrably not true (with a selftest having the
> verbose working test case in a later commit), with the following pseudo
> code:

> 	r0 = bpf_map_lookup_elem(&map, ...); // id=1
> 	r6 = r0;
> 	r0 = bpf_map_lookup_elem(&map, ...); // id=2
> 	r7 = r0;

> 	bpf_spin_lock(r1=r6);
> 	if (cond) // unknown scalar, hence verifier cannot predict branch
> 		r6 = r7;
> 	p:
> 	bpf_spin_unlock(r1=r7);

> In the first exploration path, we would want the verifier to skip
> over the r6 = r7 assignment so that it reaches BPF_EXIT and the
> state branches counter drops to 0 and it becomes a safe verified
> state.

> The branch target 'p' acts a pruning point, hence states will be
> compared. If the old state was verified without assignment, it has
> r6 with id=1, but the new state will have r6 with id=2. The other
> parts of register, stack, and reference state and any other verifier
> state compared in states_equal remain unaffected by the assignment.

> Now, when the memcmp fails for r6, the verifier drops to the switch case
> and simply memcmp until the id member, and requires the var_off to be
> more permissive in the current state. Once establishing this fact, it
> returns true and search is pruned.

> Essentially, we end up calling unlock for a bpf_spin_lock that was never
> locked whenever the condition is true at runtime.

> To fix this, also include id in the memcmp comparison. Since ref_obj_id
> is never set for PTR_TO_MAP_VALUE, change the offsetof to be until that
> member.

> Note that by default the reg->id in case of PTR_TO_MAP_VALUE should be 0
> (without PTR_MAYBE_NULL), so it should only really impact cases where a
> bpf_spin_lock is present in the map element.

> Fixes: d83525ca62cf ("bpf: introduce bpf_spin_lock")
> Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>

Acked-by: Stanislav Fomichev <sdf@google.com>

Sounds convincing. Also run the selftest to make sure it fails w/o this
patch.

> ---
>   kernel/bpf/verifier.c | 33 +++++++++++++++++++++++++++------
>   1 file changed, 27 insertions(+), 6 deletions(-)

> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 264b3dc714cc..7e6bac344d37 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -11559,13 +11559,34 @@ static bool regsafe(struct bpf_verifier_env  
> *env, struct bpf_reg_state *rold,

>   		/* If the new min/max/var_off satisfy the old ones and
>   		 * everything else matches, we are OK.
> -		 * 'id' is not compared, since it's only used for maps with
> -		 * bpf_spin_lock inside map element and in such cases if
> -		 * the rest of the prog is valid for one map element then
> -		 * it's valid for all map elements regardless of the key
> -		 * used in bpf_map_lookup()
> +		 *
> +		 * 'id' must also be compared, since it's used for maps with
> +		 * bpf_spin_lock inside map element and in such cases if the
> +		 * rest of the prog is valid for one map element with a specific
> +		 * id, then the id in the current state must match that of the
> +		 * old state so that any operations on this reg in the rest of
> +		 * the program work correctly.
> +		 *
> +		 * One example is a program doing the following:
> +		 *	r0 = bpf_map_lookup_elem(&map, ...); // id=1
> +		 *	r6 = r0;
> +		 *	r0 = bpf_map_lookup_elem(&map, ...); // id=2
> +		 *	r7 = r0;
> +		 *
> +		 *	bpf_spin_lock(r1=r6);
> +		 *	if (cond)
> +		 *		r6 = r7;
> +		 * p:
> +		 *	bpf_spin_unlock(r1=r6);
> +		 *
> +		 * The label 'p' is a pruning point, hence states for that
> +		 * insn_idx will be compared. If we don't compare the id, the
> +		 * program will pass as the r6 and r7 are otherwise identical
> +		 * during the second pass that compares the already verified
> +		 * state with the one coming from the path having the additional
> +		 * r6 = r7 assignment.
>   		 */
> -		return memcmp(rold, rcur, offsetof(struct bpf_reg_state, id)) == 0 &&
> +		return memcmp(rold, rcur, offsetof(struct bpf_reg_state, ref_obj_id))  
> == 0 &&
>   		       range_within(rold, rcur) &&
>   		       tnum_in(rold->var_off, rcur->var_off);
>   	case PTR_TO_PACKET_META:
> --
> 2.38.1