eBPF

Started 2026-02-24

Marketed as JavaScript for the Kernel, eBPF is a technology that helps extend the Linux kernel without modifying and recompiling the kernel itself. Think of browser plugins.

eBPF is closely related to my research. I intend this section to be directory of eBPF-related resources with personal notes and explanations.

Documentation

Tutorials

eBPF Verifier

The Linux kernel has a component called the eBPF verifier which performs various safety and security checks on eBPF programs before letting them execute in the privileged context of the kernel.

  • verifier.c, verifier.h -- the main source files of the verifier
  • Verifier documentation -- not very organized, but it contains some details on register value tracking, register liveness tracking, pruning, and more. It also contains some examples to help understand the cryptic error messages produced by the verifier, which is often a source of criticism.
  • Complexity of the BPF Verifier -- discusses the growth in size and cyclomatic complexity of the verifier over time. Lists top ten most complex functions (mainly checks) in the verifier.
  • [VIDEO] Peeking into the eBPF verifier, Shung-Hsi Yu, 2022 -- A five minute presentation by a SUSE engineer with a couple of examples illustrating the type checking and bounds checking performed by the verifier.
  • [VIDEO] More than you want to know about BPF verifier, Shung-Hsi Yu, 2022 -- A 43-minute talk discussing:
    • 05:50 -- eBPF VM state tracking, data types, eBPF context, calling convention
    • 11:24 -- composite types
    • 13:05 -- stack tracking
    • 14:36–18:28 -- value tracking ("most important concept", but nothing new if you are already familiar with abstract interpretation)
    • 18:28 -- tristate numbers, 22:39 -- intervals and tnums are used together
    The rest of the talk contains an example, Q&A, some interesting topics (30:38), and a discussion on bugs. One interesting fact is that the verifier not just verifies a program, but modifies it as well (as part of Spectre mitigration, for example).
  • SIGCOMM 2023 workshop slides, Daniel Borkmann, 2023 -- slide 44 onwards discussing eBPF verifier and open problems

Research