Incorrect context descriptor classification

[Maxime-Derri]

It appears that the precision has decreased compared to previous versions that did not use a separated domain for types.
I observed a case where, for the same program, type information no longer seems to be tracked with the latest version of PREVAIL, leading the verifier to return an empty abstract state (bottom).

A test is provided with this issue. the following program ex_precision.zip:

• section: fexit/bpf_testmod_fentry_test11
• function: test2

was previously accepted, but is now rejected.

[elazarg]

Thanks for the report!

After digging into it, this regression turns out not to be caused by the recent separation of the type and numeric domains (which we already knew would reduce precision), but by a misclassification of the program type.

The actual issue is that PREVAIL misclassifies this fentry/fexit BPF tracing program as a socket_filter program, and therefore assigns it a sk_buff-style context descriptor with .end = 80. Under that descriptor, the load from ctx[80] is treated as may_touch_ptr, so the new ctx-load transformer conservatively havocs the type of the destination register's instead of marking it as a number.

The actual context is described here: https://docs.ebpf.io/linux/program-type/BPF_PROG_TYPE_RAW_TRACEPOINT/

Context
The context for raw tracepoint programs is a pointer to a struct bpf_raw_tracepoint_args:

struct bpf_raw_tracepoint_args {
       __u64 args[0];
};
The args array contains the raw arguments to the tracepoint. The number of arguments is determined by the tracepoint.
The verifier will enforce that the number of arguments matches the number of arguments expected by the tracepoint.
The BPF program can cast the u64 values to the expected types or use the bpf_probe_read/bpf_probe_read_kernel
helper function to read the arguments.

I believe the old behavior was simply unsound with respect to the actual descriptor of fentry/fexit.

In general, the handling of context descriptors need to be systematically corrected.