[PATCH bpf v1 0/2] Fix map value pruning check

[PATCH bpf v1 0/2] Fix map value pruning check

[Kumar Kartikeya Dwivedi]

While digging into related code for spin lock correctness, the pruning
related checks for PTR_TO_MAP_VALUE in regsafe looked suspect. The
reg->id is never compared (which is preserved only in case the map value
has a bpf_spin_lock) between rold and rcur.

Turns out this allows unlocking a bpf_spin_unlock for a reg with a
different reg->id, i.e. not pairing spin lock calls correctly. A
regression test is included in patch 2.

However, looking more closely, it seems to me that the logic of
check_ids is broken as well.

Edward, given you introduced the idmap, can you provide a little more
historical context on what the idea behind check_ids was, since it seems
to be doing the wrong thing as far as I understood things. I think we
need to compare the ids directly everywhere.

For instance, when we have a case like below:

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

Only r6 differs between old and cur at pruning point p. If we did the
check in patch 1 using check_ids, it would end up seeing that no mapping
exists for old id so it will set up mapping of 1 to 2, and then return
true.

I think similar problems exist elsewhere where after establishing the
first mapping, if there are no more lookups into idmap, it will just
pass the states_equal check.

We are already inconsistent in other places, since if it made sense
states_equal should have been using check_ids logic for active_spin_lock
checks (but it's not a bug in that case, just more conservative).

If we agree it needs fixing, I will send a separate fix removing its use
from regsafe. For now this patch should address the bpf_spin_lock issue.

Kumar Kartikeya Dwivedi (2):
  bpf: Fix state pruning check for PTR_TO_MAP_VALUE
  selftests/bpf: Add pruning test case for bpf_spin_lock

 kernel/bpf/verifier.c                         | 33 +++++++++++++---
 .../selftests/bpf/verifier/spin_lock.c        | 39 +++++++++++++++++++
 2 files changed, 66 insertions(+), 6 deletions(-)


base-commit: 5704bc7e8991164b14efb748b5afa0715c25fac3
-- 
2.38.1

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

[Kumar Kartikeya Dwivedi]

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

[PATCH bpf v1 2/2] selftests/bpf: Add pruning test case for bpf_spin_lock

[Kumar Kartikeya Dwivedi]

Test that when reg->id is not same for the same register of type
PTR_TO_MAP_VALUE between current and old explored state, we currently
return false from regsafe and continue exploring.

Without the fix in prior commit, the test case fails.

Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>
---
 .../selftests/bpf/verifier/spin_lock.c        | 39 +++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/tools/testing/selftests/bpf/verifier/spin_lock.c b/tools/testing/selftests/bpf/verifier/spin_lock.c
index 781621facae4..0a8dcfc37fc6 100644
--- a/tools/testing/selftests/bpf/verifier/spin_lock.c
+++ b/tools/testing/selftests/bpf/verifier/spin_lock.c
@@ -331,3 +331,42 @@
 	.errstr = "inside bpf_spin_lock",
 	.prog_type = BPF_PROG_TYPE_SCHED_CLS,
 },
+{
+	"spin_lock: regsafe compare reg->id for map value",
+	.insns = {
+	BPF_MOV64_REG(BPF_REG_6, BPF_REG_1),
+	BPF_LDX_MEM(BPF_W, BPF_REG_6, BPF_REG_6, offsetof(struct __sk_buff, mark)),
+	BPF_LD_MAP_FD(BPF_REG_1, 0),
+	BPF_MOV64_REG(BPF_REG_9, BPF_REG_1),
+	BPF_ST_MEM(BPF_W, BPF_REG_10, -4, 0),
+	BPF_MOV64_REG(BPF_REG_2, BPF_REG_10),
+	BPF_ALU64_IMM(BPF_ADD, BPF_REG_2, -4),
+	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_map_lookup_elem),
+	BPF_JMP_IMM(BPF_JNE, BPF_REG_0, 0, 1),
+	BPF_EXIT_INSN(),
+	BPF_MOV64_REG(BPF_REG_7, BPF_REG_0),
+	BPF_MOV64_REG(BPF_REG_1, BPF_REG_9),
+	BPF_MOV64_REG(BPF_REG_2, BPF_REG_10),
+	BPF_ALU64_IMM(BPF_ADD, BPF_REG_2, -4),
+	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_map_lookup_elem),
+	BPF_JMP_IMM(BPF_JNE, BPF_REG_0, 0, 1),
+	BPF_EXIT_INSN(),
+	BPF_MOV64_REG(BPF_REG_8, BPF_REG_0),
+	BPF_MOV64_REG(BPF_REG_1, BPF_REG_7),
+	BPF_ALU64_IMM(BPF_ADD, BPF_REG_1, 4),
+	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_spin_lock),
+	BPF_JMP_IMM(BPF_JEQ, BPF_REG_6, 0, 1),
+	BPF_JMP_IMM(BPF_JA, 0, 0, 1),
+	BPF_MOV64_REG(BPF_REG_7, BPF_REG_8),
+	BPF_MOV64_REG(BPF_REG_1, BPF_REG_7),
+	BPF_ALU64_IMM(BPF_ADD, BPF_REG_1, 4),
+	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_spin_unlock),
+	BPF_MOV64_IMM(BPF_REG_0, 0),
+	BPF_EXIT_INSN(),
+	},
+	.fixup_map_spin_lock = { 2 },
+	.result = REJECT,
+	.errstr = "bpf_spin_unlock of different lock",
+	.prog_type = BPF_PROG_TYPE_SCHED_CLS,
+	.flags = BPF_F_TEST_STATE_FREQ,
+},
-- 
2.38.1

Re: [PATCH bpf v1 0/2] Fix map value pruning check

[Edward Cree]

On 11/11/2022 20:27, Kumar Kartikeya Dwivedi wrote:
> However, looking more closely, it seems to me that the logic of
> check_ids is broken as well.
> 
> Edward, given you introduced the idmap, can you provide a little more
> historical context on what the idea behind check_ids was, since it seems
> to be doing the wrong thing as far as I understood things. I think we
> need to compare the ids directly everywhere.

reg->id has two different kinds of usage/semantics.  One, which was
 the only one when idmap was introduced, is pairing with other regs
 within state (including stack slots and caller frames); for this,
 check_ids() is fine (the comment above it explains why).
The other, added by d83525ca62cf ("bpf: introduce bpf_spin_lock"),
 pairs not with other regs' ids but with state->active_spin_lock;
 currently states_equal() requires this to be numerically identical
 between old and cur, rather than running it through the idmap; this
 would appear to be the origin of the bug.

Alexei, is there any valid world in which there's an active_spin_lock
 but the corresponding id does not exist anywhere in the state's
 regs, stack etc.?  If not then I think it suffices to
 check_ids(old->active_spin_lock, cur->active_spin_lock,
           env->idmap_scratch);
 in func_states_equal() of the leaf frame (only leaf frame can be
 holding a spinlock), and remove the existing check from
 states_equal().
Because what we want to know isn't "Do both of these spinlocks come
 from the same original ID derivation", but "do all registers that
 hold a value that could be used to unlock the spinlock in the
 continuation-to-exit of the old state also hold such a value in the
 current state", which means that we want the pair <old_asl, new_asl>
 in the idmap when we walk the regs and stack.

While we *could* implement that by requiring IDs to match numerically
 as in Kumar's patch, that's needlessly strict and will miss pruning
 opportunities.

-ed

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

[sdf]

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

Re: [PATCH bpf v1 2/2] selftests/bpf: Add pruning test case for bpf_spin_lock

[sdf]

On 11/12, Kumar Kartikeya Dwivedi wrote:
> Test that when reg->id is not same for the same register of type
> PTR_TO_MAP_VALUE between current and old explored state, we currently
> return false from regsafe and continue exploring.

> Without the fix in prior commit, the test case fails.

> Signed-off-by: Kumar Kartikeya Dwivedi <memxor@gmail.com>

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

> ---
>   .../selftests/bpf/verifier/spin_lock.c        | 39 +++++++++++++++++++
>   1 file changed, 39 insertions(+)

> diff --git a/tools/testing/selftests/bpf/verifier/spin_lock.c  
> b/tools/testing/selftests/bpf/verifier/spin_lock.c
> index 781621facae4..0a8dcfc37fc6 100644
> --- a/tools/testing/selftests/bpf/verifier/spin_lock.c
> +++ b/tools/testing/selftests/bpf/verifier/spin_lock.c
> @@ -331,3 +331,42 @@
>   	.errstr = "inside bpf_spin_lock",
>   	.prog_type = BPF_PROG_TYPE_SCHED_CLS,
>   },
> +{
> +	"spin_lock: regsafe compare reg->id for map value",
> +	.insns = {
> +	BPF_MOV64_REG(BPF_REG_6, BPF_REG_1),
> +	BPF_LDX_MEM(BPF_W, BPF_REG_6, BPF_REG_6, offsetof(struct __sk_buff,  
> mark)),
> +	BPF_LD_MAP_FD(BPF_REG_1, 0),
> +	BPF_MOV64_REG(BPF_REG_9, BPF_REG_1),
> +	BPF_ST_MEM(BPF_W, BPF_REG_10, -4, 0),
> +	BPF_MOV64_REG(BPF_REG_2, BPF_REG_10),
> +	BPF_ALU64_IMM(BPF_ADD, BPF_REG_2, -4),
> +	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_map_lookup_elem),
> +	BPF_JMP_IMM(BPF_JNE, BPF_REG_0, 0, 1),
> +	BPF_EXIT_INSN(),
> +	BPF_MOV64_REG(BPF_REG_7, BPF_REG_0),
> +	BPF_MOV64_REG(BPF_REG_1, BPF_REG_9),
> +	BPF_MOV64_REG(BPF_REG_2, BPF_REG_10),
> +	BPF_ALU64_IMM(BPF_ADD, BPF_REG_2, -4),
> +	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_map_lookup_elem),
> +	BPF_JMP_IMM(BPF_JNE, BPF_REG_0, 0, 1),
> +	BPF_EXIT_INSN(),
> +	BPF_MOV64_REG(BPF_REG_8, BPF_REG_0),
> +	BPF_MOV64_REG(BPF_REG_1, BPF_REG_7),
> +	BPF_ALU64_IMM(BPF_ADD, BPF_REG_1, 4),
> +	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_spin_lock),
> +	BPF_JMP_IMM(BPF_JEQ, BPF_REG_6, 0, 1),
> +	BPF_JMP_IMM(BPF_JA, 0, 0, 1),
> +	BPF_MOV64_REG(BPF_REG_7, BPF_REG_8),
> +	BPF_MOV64_REG(BPF_REG_1, BPF_REG_7),
> +	BPF_ALU64_IMM(BPF_ADD, BPF_REG_1, 4),
> +	BPF_RAW_INSN(BPF_JMP | BPF_CALL, 0, 0, 0, BPF_FUNC_spin_unlock),
> +	BPF_MOV64_IMM(BPF_REG_0, 0),
> +	BPF_EXIT_INSN(),
> +	},
> +	.fixup_map_spin_lock = { 2 },
> +	.result = REJECT,
> +	.errstr = "bpf_spin_unlock of different lock",
> +	.prog_type = BPF_PROG_TYPE_SCHED_CLS,
> +	.flags = BPF_F_TEST_STATE_FREQ,
> +},
> --
> 2.38.1

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

[Andrii Nakryiko]

On Fri, Nov 11, 2022 at 12:27 PM Kumar Kartikeya Dwivedi
<memxor@gmail.com> 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>
> ---
>  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 &&

I don't think it's right to check ids exactly. I do think that this
check is missing check_ids(), though, but its unrelated to the problem
you are trying to solve.

As for the problem with spin_lock above. Again, there is nothing wrong
about doing the whole id remapping idea, it just establishes
equivalence between registers/slots without requiring absolute values
of IDs to be exact, rather it finds a consistent and correct
permutation.

I think the fix is what Ed suggested. Where we currently check

old->active_lock.ptr != cur->active_lock.ptr || old->active_lock.id !=
cur->active_lock.id

at least for IDs we should do the comparison with check_ids().


But another thing which I'm not sure about and jumped on me when I
looked at the code is that we reset ID map for each function frame,
not preserving the mapping across all frames. It might be sufficient,
but seems iffy. Also, I think we should take idmap into account when
doing refsafe(), which would require "global" idmap across all frames.

Thoughts?


>                        range_within(rold, rcur) &&
>                        tnum_in(rold->var_off, rcur->var_off);
>         case PTR_TO_PACKET_META:
> --
> 2.38.1
>