Security researchers examining the eBPF verifier encountered a case where two independent static analyzers reached opposite conclusions about the same object file. The program correlated_branch.c from the ebpf-samples repository was accepted by the external verifier PREVAIL yet rejected by the in-kernel Linux verifier during loading via bpftool.
The test was performed on Ubuntu 24.04.1 LTS with kernel Linux 6.14.0-37-generic and clang 18.1.3 targeting the bpf architecture. The XDP function ConvergedBranch first obtains packet boundaries from the context, calls check_packet to verify that at least 14 bytes are available, and only then dereferences the Ethernet header type field at offset 12.
The kernel verifier log shows that the scalar register holding the computed length receives the constraint R2_w=scalar(smin=umin=14,...) after the comparison. However, the pointer stored in r7 is not annotated with a matching packet offset range, causing the subsequent load r3 = *(u16 *)(r7 + 12) to be rejected as an invalid packet access.
In contrast, PREVAIL records the state r7.type=packet packet_size=14 r7.packet_offset=0 after the same check. When the load instruction is reached, the tool evaluates assert valid_access(r7.offset+12, width=2) and permits the read because the offset plus size fits inside the proven 14-byte region.
The root cause is architectural: the kernel verifier treats the length scalar and the packet pointer as separate abstract domains, while PREVAIL preserves relational information across states. When the bounds check was inlined directly in ConvergedBranch instead of being hidden inside check_packet, the kernel verifier successfully accepted the program.
The episode demonstrates that a verifier rejection does not automatically imply the presence of a memory-safety bug. Analysts must examine register states such as R7 pkt(off=0,r=0) to determine whether the required offset range was simply not propagated.
