The eBPF Runtime in the Linux Kernel

5 Security of eBPF Programs

The security of programs is a critical aspect of eBPF programs, ensuring that they execute correctly and safely without compromising the stability and security of the Linux kernel. In the context of eBPF programs, program security refers to a set of properties that must be satisfied to protect the runtime integrity of the kernel and maintain the invariants of the kernel context in which eBPF programs will execute. Any program that violates these security properties should be rejected when loaded into the kernel.

5.1 Security Properties

We will now categorize and discuss each security property based on the BPF verifier code and related documentation [75, 76].

• Memory Safety: The verifier strives to ensure that there are no out-of-bounds accesses, invalid or arbitrary memory accesses, and use-after-free errors for all memory regions accessible to the program. The verifier performs precise boundary tracking for all memory regions accessible to the program and checks that all accesses are within bounds. Any released memory regions must not be accessed again. Arbitrary values cannot be used as pointers for memory access.

• Type Safety: The verifier precisely knows the type of each register pointing to memory regions accessible to the program. It tracks the types of objects on the stack. This process helps avoid errors caused by type confusion and ensures that different types of programs can use various utilities without corrupting kernel memory. The verifier also utilizes BTF (§3.4) to obtain important information about the types and code of the kernel and eBPF programs. BTF helps identify eBPF kernel data structures and ensures that accesses to aggregate types (such as structures) do not exceed their allowed bounds.

• Resource Safety: The verifier checks that no resources are left behind when the program exits. This means that the program must use appropriate helper functions to release all allocated memory, acquired locks, and reference counts of kernel objects.

• Information Leak Safety: The eBPF verifier prohibits any kernel information leaks by analyzing pointers that may reference kernel memory, aiming to prevent any information from leaking into user-accessible memory regions. It performs comprehensive escape analysis [78] on all pointers that may point to kernel memory, ensuring that these pointers do not escape to user-accessible memory regions. Additionally, it rejects any attempts to read uninitialized areas on the stack.

• No Data Races: The verifier aims to ensure that access to kernel state by the program does not result in data races. It mandates that any operations on kernel state must be performed through helper functions that implement appropriate synchronization mechanisms. However, the verifier does not diagnose data races in accesses to memory owned by the program (such as values in eBPF maps) since this does not affect the runtime integrity of the kernel.

• Termination: The verifier limits the maximum number of instructions that can be explored on all paths of the program, known as the instruction complexity limit, to ensure that all programs can terminate. If a program cannot prove that all paths terminate within this limit, the verifier will reject the program. This situation may arise due to infinite loops, unbounded loops with unprovable termination conditions, or simply because the program is too large.

• No Deadlocks: The verifier aims to ensure that the program does not encounter deadlocks. By definition, a deadlock occurs when two concurrently executing programs hold two locks in opposite orders. To achieve deadlock freedom, the verifier directly prohibits the program from holding more than one lock at any time.

• Maintaining Execution Context Invariants: The verifier checks to ensure that the program can maintain all invariants in the kernel execution context. In other words, the execution of the program must not violate the invariants and assumptions of existing kernel code. This information is compiled into the verifier each time support for new kernel hooks is introduced.

By clarifying these security properties, we define the latest standards that the verifier implements for eBPF programs. However, it must be recognized that these standards are not static; rather, they are a continuous effort to protect the integrity and security of eBPF programs in the kernel and are regularly updated to reflect the dynamic nature of the field as the ecosystem evolves and new methods are explored.

5.2 eBPF Verifier

To enforce the security properties (§5.1), the eBPF verifier plays a crucial role. The eBPF verifier is a static analyzer for eBPF programs. When a program is loaded into the kernel, the verifier is invoked with the task of ensuring that the program can execute safely in the kernel context. Once the program is deemed safe, the verifier submits the bytecode to the Just-In-Time (JIT) compiler, where the bytecode is converted into native machine instructions. Subsequently, the program can be attached to one of the many available kernel hooks to begin execution.

The verifier performs static analysis of the program at the eBPF bytecode level. It has access to the BTF (§3.4) debug information of the program, which is generated during the process of compiling the program from a high-level language to eBPF bytecode. This design choice, which operates based on eBPF bytecode and BTF, allows the eBPF verifier to be used for programs written in various high-level languages.

As shown in Figure 4, the program verification process consists of four main stages. The first stage verifies the program’s control flow graph (CFG: control-flow graph) (§6). The second stage performs exhaustive symbolic execution of the program to ensure its safety (§7). Subsequently, the third stage optimizes and transforms the program before it is submitted to the Just-In-Time compiler (JIT) (§9) for final compilation (§8). The following subsections will detail each stage of the verifier, explaining how the verifier enforces the security properties.

Src

https://arxiv.org/pdf/2410.00026v2