uBPF bounds_check doesn't account for access to packet data

[Alan-Jowett]

The bounds_check function doesn't correctly account for programs that access packet data.

As an example, xdp_md_t is defined as:

// XDP hook.  We use "struct xdp_md" for cross-platform compatibility.
typedef struct xdp_md
{
    void* data;         /*     0     8 */
    void* data_end;     /*     8     8 */
    uint64_t data_meta; /*     16    8 */

    /* size: 12, cachelines: 1, members: 3 */
    /* last cacheline: 12 bytes */
} xdp_md_t;

Programs are legal permitted to access memory pointed to by context->data up to context->data_end.

But the bounds_check only checks for:

1. Access is within range of [context, context+sizeof(context)]
2. Access is within range [stack, stack+stack_size]

[Alan-Jowett]

Note: This also misses cases where we access memory retrieved from a map.

[jpsamaroo]

These are the sorts of things that we really need a verifier for (and I imagine that's what PREVAIL does for Windows eBPF). With that, we'd also need some way to tell the verifier about input structures; a BTF parser would probably make sense to accomplish that.

[Alan-Jowett]

The model we are taking with Ebpf-on-Windows is to define all the inputs to types of eBPF programs and the signature of helper functions and have that provided to the verifier at verification time. See: eBpfExtensions

Unfortunately, the bounds_check code as it exists today is of limited usefulness.

[rlane]

Yeah, the current bounds check is very simplistic. Does the PREVAIL verifier enforce that the code does its own bounds checking?

[Alan-Jowett]

Yep, Prevail tracks each BPF register and evaluates the control flow graph to determine safety. Not an expert on this myself, but based on my understanding a formal verification.

[Alan-Jowett]

This was fixed with the addition of the ubpf_register_data_bounds_check function.