vbpf / prevail / 29018859372

push

github

Model direct socket reads conservatively

After stale type-dependent numeric facts are discarded, previously
hidden paths reach socket-returning helpers such as skc_lookup_tcp().
Those helpers can produce a non-null T_SOCKET, and real accepted
programs read fields such as `state` from that socket value. Before this
change the checker required dereference sources to be
{ctx, stack, packet, shared}, so a valid socket read was rejected as a
type error.

Give T_SOCKET its own direct-access rule instead of pretending it is one
of the existing pointer kinds:

- Introduce a generic EbpfStructFieldDescriptor/EbpfStructDescriptor
  typed-memory access model (src/spec/type_descriptors.hpp) and describe
  the safe common bpf_sock field subset with it. The existing packet-
  pointer ctx-write overlap logic is refactored through the same
  write_may_touch_readonly_field helper.
- Split TypeGroup::pointer (ctx|packet|stack|shared, region pointers with
  modeled arithmetic) from a new TypeGroup::dereferenceable
  (+socket +alloc_mem), whose members are load/store-checkable.
- Socket memory is read-only, precise-offset, in-struct-bounds, and
  null-checked unless or_null; contents remain havoced. The kernel's
  32-bit read at dst_port is modeled via extra_read_width_at_start.
- Atomics now gate on dereferenceable and havoc r0/src for non-stack
  memory, so T_ALLOC_MEM fetch/CMPXCHG no longer leave stale constants;
  atomic writes to a read-only socket are still rejected.
- Initialize socket_offset for socket-returning helpers so later access
  checks do not depend on stale or absent kind facts.

Part of the #1152 stack; does not close #1152 by itself.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

60 of 64 new or added lines in 4 files covered. (93.75%)

9313 of 10748 relevant lines covered (86.65%)

6391920.93 hits per line