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

Message

Kumar Kartikeya Dwivedi Nov. 11, 2022, 8:27 p.m. UTC

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

Comments

Edward Cree Nov. 11, 2022, 9:17 p.m. UTC | #1

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