The eBPF Verifier - How Linux Safely Runs User Code in Kernel Space

Understanding how the Linux kernel can safely run user-supplied programs without risking system stability through eBPF's mathematical verification system.
Jon Friesen
Jon Friesen
September 2, 2025

Running arbitrary code in kernel space. If you've been in operations long enough, that sentence probably just triggered your fight-or-flight response. And for good reason—kernel modules have been causing production outages since before containers were cool.

But eBPF is different. Not "marketing different" but architecturally, fundamentally, mathematically different. Today we're going to dig deep into how the Linux kernel can safely run user-supplied programs without risking system stability. This isn't about any specific tool or vendor—it's about understanding why eBPF has become the kernel's preferred extension mechanism.

The Challenge: Extending the Kernel Without Breaking It

The Linux kernel needs to be extensible. Whether it's for observability, networking, or security, we need ways to add functionality without recompiling the kernel or loading risky modules. Historically, we had three options:

  1. Kernel modules: 😱 Full access, full risk
  2. Userspace polling: 😴 Safe but slow
  3. Kernel patches: 😰 Safe-ish but requires recompilation

Each approach involved trading off between safety, performance, and flexibility. Then eBPF came along and changed the game entirely.

The eBPF Architecture: Verified Code in a Sandbox

eBPF (extended Berkeley Packet Filter) allows you to run custom programs in kernel space, but with a twist: every program must pass through a verifier that proves it's safe before it can run. Let's break down how this works.

The Verifier: Your Mathematical Proof of Safety

The eBPF verifier is the heart of what makes eBPF safe. It's not just a linter or static analyzer—it's an abstract interpreter that simulates all program paths to ensure safety. Here's what it checks:

// Example: The verifier tracks EVERY possible code path
void* ptr = map_lookup_elem(&my_map, &key);
// The verifier knows ptr might be NULL
if (condition) {
    // Path 1: verifier tracks that we checked ptr
    if (ptr != NULL) {
        value = *ptr;  // Safe: verifier knows ptr is valid here
    }
} else {
    // Path 2: different code path
    value = *ptr;  // REJECTED: ptr might be NULL on this path
}

The verifier performs several types of analysis:

1. Control Flow Analysis

// The verifier ensures no infinite loops
for (int i = 0; i < 100; i++) {  // OK: bounded loop
    // do work
}

while (condition) {  // REJECTED: unbounded loop
    // this will never load
}

The verifier builds a complete control flow graph and ensures:

  • Every path through the program terminates
  • No backward jumps that could create infinite loops (unless bounded)
  • Maximum instruction count isn't exceeded (1 million for privileged programs)

Note: The instruction count limit is higher for privileged programs—up to 1 million instructions. For unprivileged programs, it is typically limited to 10,000.

2. Memory Safety Verification

// The verifier tracks the size and validity of every memory region
struct sk_buff *skb = ctx;  // ctx is validated by program type

// Verifier knows skb->data and skb->data_end boundaries
void *data = (void *)(long)skb->data;
void *data_end = (void *)(long)skb->data_end;

// Must check bounds before access
if (data + sizeof(struct ethhdr) > data_end)
    return DROP;  // Verifier requires this check

struct ethhdr *eth = data;  // Now safe to access

For every memory access, the verifier ensures:

  • Pointers are valid (not NULL unless explicitly checked)
  • Array bounds are respected
  • Stack doesn't overflow (512 bytes limit)
  • No out-of-bounds reads or writes

3. Type and Context Tracking

The verifier maintains a state machine that tracks the type and range of every register and stack slot at every program point:

// Verifier tracks types through the program
int key = 5;
struct value *val;

// After this call, verifier knows val might be NULL
val = bpf_map_lookup_elem(&my_map, &key);

// Type confusion is impossible - verifier tracks that val 
// is either NULL or a pointer to struct value
if (val) {
    // Verifier knows val is non-NULL here
    val->counter++;  // Safe
}
// Verifier knows val might be NULL here
// val->counter++;  // Would be REJECTED

The JIT Compiler: From Bytecode to Native Code

Once verified, eBPF bytecode is compiled to native machine code by the Just-In-Time (JIT) compiler. This happens after verification, so even JIT bugs can't introduce unsafe behavior—the bytecode is already proven safe.

The JIT compiler also adds runtime protections:

  • Speculative execution barriers (Spectre mitigation)
  • Constant blinding (JIT spraying mitigation)
  • Tail call limits (stack overflow prevention)

Runtime Boundaries: The Sandbox in Action

Even after verification, eBPF programs run in a restricted environment:

Helper Functions: The Only Syscalls You Get

eBPF programs can't make arbitrary system calls. Instead, they can only call pre-approved helper functions:

// You can't do this:
open("/etc/passwd", O_RDONLY);  // No arbitrary syscalls

// You can only do this:
bpf_map_lookup_elem(&my_map, &key);  // Pre-approved helper
bpf_probe_read_user(&data, sizeof(data), user_ptr);  // Another helper

Each helper function is carefully implemented to be safe even if called with invalid arguments. The verifier also ensures you're calling helpers correctly based on your program type. Helper functions are whitelisted per program type. You can't call a tracing helper from an XDP program, for instance.

Maps: Structured Data Sharing

eBPF programs communicate with userspace through maps—fixed-size data structures that both sides can access:

// Kernel side (eBPF program)
struct bpf_map_def SEC("maps") events = {
    .type = BPF_MAP_TYPE_RINGBUF,
    .max_entries = 256 * 1024,
};

// Safe, bounded write to ring buffer
bpf_ringbuf_output(&events, &event, sizeof(event), 0);

// Userspace side
ring := bpf.OpenRingBuffer(eventsMap)
for {
    record, err := ring.Read()
    // Process events safely in userspace
}

Maps provide:

  • Bounded memory usage (size defined at creation)
  • Atomic operations (no data races)
  • Type safety (verifier ensures correct usage)

This means that map access must be bounded and deterministic, otherwise the verifier will reject the program.

Failure Modes: What Happens When Things Go Wrong

Let's examine specific failure scenarios and how eBPF handles them:

Scenario 1: Buggy Program Logic

// BUG: Forgot to check if ptr is NULL
void *ptr = bpf_map_lookup_elem(&my_map, &key);
int value = *(int*)ptr;  // Potential NULL dereference

What happens: Verifier rejects the program at load time
System impact: Zero—program never runs
Error message: "invalid mem access 'map_value_or_null'"

Scenario 2: Resource Exhaustion Attempt

// Attempting to consume excessive CPU
for (int i = 0; i < 1000000; i++) {
    expensive_operation();
}

What happens: Verifier rejects due to instruction limit
System impact: Zero—program never loads
Error message: "BPF program is too large. Processed 1000001 insn"

Scenario 3: Helper Function Abuse

// Trying to send signals to arbitrary processes
for (int pid = 1; pid < 65536; pid++) {
    bpf_send_signal(pid, SIGKILL);  // Trying to kill everything
}

What happens:

  1. Verifier checks if program has CAP_SYS_ADMIN
  2. Even if allowed, helper has built-in rate limiting
  3. Operations are logged for audit

System impact: Limited by helper implementation safeguards

Note: Even if allowed by the verifier, helpers like bpf_send_signal() are gated by program type, capabilities (CAP_SYS_ADMIN), and may include runtime limits to prevent abuse.

Scenario 4: Memory Corruption Attempt

// Trying to write beyond buffer bounds
char buffer[64];
for (int i = 0; i < 128; i++) {
    buffer[i] = 'A';  // Buffer overflow attempt
}

What happens: Verifier rejects at load time
System impact: Zero
Error message: "invalid stack off=-65 size=1"

Performance Characteristics: The Cost of Safety

The verifier and runtime checks do have a cost, but it's surprisingly small:

Verification Time

  • Simple programs: < 1ms
  • Complex programs: 10-100ms
  • Happens once at load time

Runtime Overhead

Native C code:         1.0x (baseline)
eBPF code:            1.1-1.2x
Kernel module:        1.0x (but no safety)
Userspace polling:    10-100x

Memory Overhead

  • Program size: Limited to ~1MB of bytecode
  • Stack: 512 bytes per program
  • Maps: Explicitly bounded at creation

The Mathematics Behind Safety

The verifier uses abstract interpretation to prove safety properties. For each instruction, it maintains abstract state:

State = {
    R0: {type: SCALAR, range: [0, 100]},
    R1: {type: PTR_TO_MAP_VALUE, offset: 0, size: 64},
    R2: {type: PTR_TO_CTX},
    ...
    Stack: [{slot: -8, type: SCALAR}, ...]
}

For each possible path through the program, the verifier:

  1. Propagates abstract state forward
  2. Checks safety at each instruction
  3. Ensures all paths converge to safe states

This is similar to how Rust's borrow checker proves memory safety at compile time, except the eBPF verifier works on bytecode at load time.

eBPF in Production: Real-World Applications

This mathematical approach to safety is why major projects are betting on eBPF:

  • Cilium uses eBPF for container networking and security
  • Falco leverages eBPF for runtime security monitoring
  • systemd employs eBPF for system observability
  • Cloud providers run customer eBPF programs with confidence

At Qpoint, we use eBPF to provide deep visibility into external API traffic without compromising system stability. Our Qtap platform leverages eBPF's safety guarantees to monitor outbound connections at the kernel level, giving teams unprecedented insight into their external dependencies.

The Bottom Line

eBPF represents a fundamental shift in how we think about kernel extensibility. Instead of choosing between safety and performance, eBPF gives us both through static verification and runtime sandboxing. The verifier isn't just a safety check—it's a proof system that ensures your program cannot violate kernel integrity.

This is why major projects like Qpoint, Cilium, Falco, and systemd are betting on eBPF. It's why cloud providers are comfortable running customer eBPF programs. And it's why the Linux kernel community has embraced eBPF as the preferred way to extend kernel functionality.

The next time someone asks you about running code in kernel space, you can explain that eBPF programs are closer to mathematical proofs than traditional code. They're not just "probably safe"—they're "prove"-ably safe.

Want to go deeper? Check out the kernel's verifier documentation, browse the verifier source, or read the ✨amazing✨ eBPF Verifier Code Review by the NCC Group. Hopefully, this article alongside these resources help making the decision for you to start taking advantage of the immense power of eBPF enabled programs in production!

Inspired? Share the eBPF gospel with your kids! The Illustrated Children's Guide to eBPF 🐝

Ready to see eBPF in action? Schedule a demo with a Qpoint solution engineer and discover how eBPF-powered observability can transform your understanding of external API traffic.