Re: [PATCH bpf-next 1/9] bpf: introduce bpf_spin_lock

[Alexei Starovoitov <alexei.starovoitov@gmail.com>]

On Thu, Jan 17, 2019 at 12:27:55PM +0100, Daniel Borkmann wrote:
> 
> Was thinking something like this, in very rough pseudo code:
> 
> Prog A (normal spin lock use of mapA):
> 
>   val = bpf_map_lookup_elem(&mapA, &key);
>   if (val) {
>     bpf_spin_lock(&val->lock);
>     [...]
>     bpf_spin_unlock(&val->lock);
>   }
> 
> Prog B:
> 
>   if (non_const_condition_A) {
>     map_ptr = &mapB;   // mapB is normal array map with same
>                        // properties as mapA, but no BTF and
>                        // thus no spinlock use.
>   } else {
>     map_ptr = &mapA;
>   }
>   val = bpf_map_lookup_elem(&map_ptr, &key);
>   map_ptr = 0; // clear map reg to match for
>                // both verification paths
>   if (val) {
>     // turning val into PTR_TO_MAP_VALUE
>     if (non_const_condition_B) {
>       // write into memory area of spin_lock;
>       // first path with mapB is considered
>       // safe (since map with no spin_lock so
>       // write into this area allowed);
>       // now when verifier is checking the
>       // non_const_condition_A's else path
>       // with mapA, then non_const_condition_B
>       // has pruning checkpoint and is going
>       // to compare reg with PTR_TO_MAP_VALUE;
>       // since id is not considered I /think/
>       // verifier would find it (wrongly) safe
>       // as well.
>     }
>   }
> 
> Wdyt?

I've implemented it and it was rejected.
regsafe() is doing:
memcmp(rold, rcur, offsetof(struct bpf_reg_state, id));
'map_ptr' is before 'id' in bpf_reg_state.
lookups from different maps will have different register states
as expected.

I still felt that we need to compare id, so I tried
if (random)
   val = bpf_map_lookup_elem(&hash_map, &key1);
else
   val = bpf_map_lookup_elem(&hash_map, &key2);

to force pruning of two states that point to the same map.
The val->spin_lock addresses will be different and intuitively it
may feel that we need to compare id, but it's unnecessary.
If the rest of the program is valid with val for key1
it's a good thing to prune verification for key2 to avoid
spending more cycles in the verifier.
All map elements have spin_locks. If bpf code is valid
for one element it's valid for all elements.

Then I tried to trick the verifier with the following:

int flag = 0;
if (random) {
   val = bpf_map_lookup_elem(&hash_map, &key1);
} else {
   flag = 1;
   val = bpf_map_lookup_elem(&hash_map, &key2);
}

if (!val)
  goto err;
bpf_spin_lock(&val->lock);
bpf_spin_unlock(&val->lock);
if (flag == 1) // access spin_lock with ld/st

the first pass of the verifier will correctly avoid
exploring 'flag == 1' condition (because the verifier is
smart enough to know that the flag is 0 there), but
the second pass with different reg->id for 'val' will not be pruned,
since the register (or stack) where 'flag' is stored
is different and the verifier will proceed and will
catch ld/st into spin_lock field and the prog will be rejected.

So I believe the verifier should not compare 'id' in regsafe()
for PTR_TO_MAP_VALUE to have better pruning.
I'll add a comment there explaining this.