eBPF Verifier's Design Principles

[Patrick ZHANG]

Hi there,
I am not sure I am doing this in the right way.
I writing to seek your guidance and expertise regarding on kernel security.
Specifically, my focus has been on the eBPF environment and its verifier,
which plays a crucial role in ensuring kernel safety.

While conducting my research, I discovered that there are no official
documents available that outline the principles of the verifier.
Consequently, I have endeavored to deduce the kernel safety principles
ensured by the verifier by studying its code. Based on my analysis, I
have identified the following principles:
1. Control Flow Integrity: It came to my attention that the verifier
rejects BPF programs containing indirect call instructions (callx). By
disallowing indirect control flow, the verifier ensures the identification
of all branch targets, thereby upholding control flow integrity (CFI).

2. Memory Safety: BPF programs are restricted to accessing predefined
data, including the stack, maps, and the context. The verifier effectively
prevents out-of-bounds access and modifies memory access to thwart
Spectre attacks, thus promoting memory safety.

3. Prevention of Information Leak: Through a comprehensive analysis of
all register types, the verifier prohibits the writing of pointer-type
registers
into maps. This preventive measure restricts user processes from reading
kernel pointers, thereby mitigating the risk of information leaks.

4. Prevention of Denial-of-Service (DoS): The verifier guarantees the
absence of deadlocks and crashes (e.g., division by zero), while also
imposing a limit on the execution time of BPF programs (up to 1M
instructions). These measures effectively prevent DoS attacks.

I would greatly appreciate it if someone could review the aforementioned
principles to ensure their accuracy and comprehensiveness. If there are
any additional principles that I may have overlooked, I would be grateful
for your insights on this matter.

Furthermore, I would like to explore why the static verifier was chosen as
the means to guarantee kernel security when there are other sandboxing
techniques that can achieve kernel safety by careful design.

The possible reasons I can think of are that verified (and jitted) BPF
programs can run at nearly native speed, and that eBPF inherits the verifier
from cBPF for compatibility reasons.

Thank you very much for your time and attention. I appreciate the  feedback
and insights.

Best,
Patrick