[RFC PATCH 0/1] bpf, docs: structured overview of verifier

[RFC PATCH 0/1] bpf, docs: structured overview of verifier

[Burak Emir]

This is an RFC for adding overview documentation for the BPF verifier.

The existing verifier.rst has detail but IMHO it lacks structure and
background. Here is my humble proposal to make the verifier docs
more helpful for newcomers.

Finding a balance between overview and detail in documentation is 
never easy. The idea here is to describe abstract interpretation and have
enough information that anyone interested can learn what is going on. 

Please let me know what you think. I used Gemini 3 to get a first draft,
which I then checked word-for-word and reworked.

Burak Emir (1):
  bpf, docs: structured docs for the verifier

 Documentation/bpf/index.rst                   |  1 +
 .../bpf/verifier-overview-1-abstr-interp.rst  | 74 +++++++++++++++
 .../bpf/verifier-overview-2-domain.rst        | 91 +++++++++++++++++++
 .../bpf/verifier-overview-3-dataflow.rst      | 83 +++++++++++++++++
 .../bpf/verifier-overview-4-pruning.rst       | 59 ++++++++++++
 .../bpf/verifier-overview-5-advanced.rst      | 70 ++++++++++++++
 Documentation/bpf/verifier-overview-index.rst | 17 ++++
 7 files changed, 395 insertions(+)
 create mode 100644 Documentation/bpf/verifier-overview-1-abstr-interp.rst
 create mode 100644 Documentation/bpf/verifier-overview-2-domain.rst
 create mode 100644 Documentation/bpf/verifier-overview-3-dataflow.rst
 create mode 100644 Documentation/bpf/verifier-overview-4-pruning.rst
 create mode 100644 Documentation/bpf/verifier-overview-5-advanced.rst
 create mode 100644 Documentation/bpf/verifier-overview-index.rst

-- 
2.53.0.473.g4a7958ca14-goog

[RFC PATCH 1/1] bpf, docs: structured docs for the verifier

[Burak Emir]

Multi-part docseries (verifier-formal-*.rst) for BPF verifier.

Provides some background that helps get a structured overview of
the static analysis that happens in the verifier.

The documentation covers:
* Part 1: Abstract Interpretation
* Part 2: Abstract Domain (Value lattices, tnum, pointer provenance)
* Part 3: Data Flow (Transfer functions, ALU ops, bounds tracking)
* Part 4: Pruning (State equivalence, subsumption, liveness)
* Part 5: Advanced Contexts (BTF, concurrency, reference tracking)

Signed-off-by: Burak Emir <bqe@google.com>
Assisted-by: Gemini:gemini-3.1-pro,gemini-3-flash
---
 Documentation/bpf/index.rst                   |  1 +
 .../bpf/verifier-overview-1-abstr-interp.rst  | 74 +++++++++++++++
 .../bpf/verifier-overview-2-domain.rst        | 91 +++++++++++++++++++
 .../bpf/verifier-overview-3-dataflow.rst      | 83 +++++++++++++++++
 .../bpf/verifier-overview-4-pruning.rst       | 59 ++++++++++++
 .../bpf/verifier-overview-5-advanced.rst      | 70 ++++++++++++++
 Documentation/bpf/verifier-overview-index.rst | 17 ++++
 7 files changed, 395 insertions(+)
 create mode 100644 Documentation/bpf/verifier-overview-1-abstr-interp.rst
 create mode 100644 Documentation/bpf/verifier-overview-2-domain.rst
 create mode 100644 Documentation/bpf/verifier-overview-3-dataflow.rst
 create mode 100644 Documentation/bpf/verifier-overview-4-pruning.rst
 create mode 100644 Documentation/bpf/verifier-overview-5-advanced.rst
 create mode 100644 Documentation/bpf/verifier-overview-index.rst

diff --git a/Documentation/bpf/index.rst b/Documentation/bpf/index.rst
index 0d5c6f659266..3b34549f60ad 100644
--- a/Documentation/bpf/index.rst
+++ b/Documentation/bpf/index.rst
@@ -13,6 +13,7 @@ that goes into great technical depth about the BPF Architecture.
    :maxdepth: 1
 
    verifier
+   verifier-overview-index
    libbpf/index
    standardization/index
    btf
diff --git a/Documentation/bpf/verifier-overview-1-abstr-interp.rst b/Documentation/bpf/verifier-overview-1-abstr-interp.rst
new file mode 100644
index 000000000000..d6ca0ecdfeca
--- /dev/null
+++ b/Documentation/bpf/verifier-overview-1-abstr-interp.rst
@@ -0,0 +1,74 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+==============================
+Abstract Interpretation in BPF
+==============================
+
+The BPF verifier is a security boundary of the Linux kernel's BPF subsystem. Its goal is to ensure that user-provided bytecode is safe to execute in kernel space. To achieve this, it must guarantee two properties:
+
+1. **Termination:** The program must halt in a bounded amount of time (no infinite loops).
+2. **Safety:** The program must not perform illegal operations, such as out-of-bounds memory accesses, leaking uninitialized kernel memory, or dereferencing invalid pointers.
+
+BPF relies on **Static Analysis** to enforce these properties before the program is ever executed. Specifically, it uses an approach grounded in **Abstract Interpretation**.
+
+1. What is Abstract Interpretation?
+====================================
+
+Abstract interpretation is a theory of sound approximation of the semantics of computer programs. Instead of executing the program with concrete values (e.g., executing `r1 = 5`), the verifier "executes" the program using *abstract values* that represent sets of possible concrete values (e.g., executing `r1 = [1, 10]`, meaning `r1` holds some value between 1 and 10).
+
+This allows the verifier to reason about all possible execution paths simultaneously. If an operation is proven safe for the entire abstract domain (all possible values the abstract state represents), it is guaranteed to be safe for any specific concrete execution at runtime.
+
+2. The Abstract State (``struct bpf_verifier_state``)
+=====================================================
+
+In PL theory, a program state at any given instruction is a mapping of memory locations to their current values. In the BPF verifier, the abstract state is represented by ``struct bpf_verifier_state`` (defined in ``include/linux/bpf_verifier.h``).
+
+The abstract state consists of:
+
+* **Registers:** The 11 BPF registers (``r0`` - ``r10``), modeled by ``struct bpf_reg_state``.
+* **Stack:** The program's stack memory, modeled as an array of ``struct bpf_stack_state``.
+* **Call Frames:** For inter-procedural analysis, the state tracks the current function call depth and the state of the caller.
+* **Reference State:** A list of acquired resources (e.g., socket references, spinlocks) that must be released before the program terminates.
+
+Whenever the verifier steps through an instruction (executed primarily within the main verification loop of ``do_check()`` and the instruction-level evaluator ``do_check_insn()`` in ``kernel/bpf/verifier.c``), it takes the current ``struct bpf_verifier_state`` and applies a **Transfer Function** (which we will cover in Part 3) to produce a new abstract state.
+
+3. Control Flow Graph (CFG) Construction
+========================================
+
+Before analyzing data flow, the verifier must understand the control flow of the program. This is handled by ``check_cfg()`` in ``kernel/bpf/verifier.c``.
+
+It is important to note that the verifier does not construct an explicit ``Graph`` data structure. Instead, the CFG is **implicit** in the instruction set, and the verifier computes metadata over this implicit graph. The results are maintained within the ``cfg`` member of ``struct bpf_verifier_env``:
+
+* **``insn_stack``**: The stack used for the non-recursive Depth-First Search (DFS) traversal.
+* **``insn_state``**: An array tracking the DFS state of each instruction (e.g., ``DISCOVERED``, ``EXPLORED``).
+* **``insn_postorder``**: A vector of instruction indexes sorted in post-order. This is used in the **Liveness Analysis** phase (a backward data-flow analysis) performed later, for iterating through instructions efficiently.
+
+During this traversal, the verifier checks for:
+
+* **Unreachable Instructions:** Code that can never be executed.
+* **Out-of-Bounds Jumps:** Jumps that land outside the program boundaries.
+* **Back-edges (Loops):** A back-edge is a jump to an instruction that is currently on the DFS path.
+
+**Termination and Safety:**
+
+The verifier's approach to termination depends on the user's privilege level:
+
+* **Unprivileged Users**: The verifier still strictly rejects all back-edges during ``check_cfg()``. This ensures that the program is a Directed Acyclic Graph (DAG), trivially guaranteeing termination.
+* **Privileged Users (BPF_CAPABLE)**: Back-edges are permitted during the CFG phase. Termination is instead guaranteed during the **Path Exploration** phase (discussed below) by a global **Complexity Limit** (currently 1 million instructions processed). If the verifier exceeds this limit without converging, the program is rejected.
+
+If any fundamental structural error is found during this phase (e.g., an unprivileged back-edge or an out-of-bounds jump), ``check_cfg()`` returns an error, and the verifier **immediately halts analysis and rejects the program**, skipping the much more expensive data-flow analysis.
+
+4. Path Exploration vs. Data Flow Joins
+=======================================
+
+When a program branches (e.g., ``if (r1 > 10) goto A; else goto B;``), the execution path splits.
+
+In classical Abstract Interpretation, the analysis often follows both paths and then *joins* the abstract states together where the control flow merges (e.g., taking the union of the abstract values). This is fast but loses precision.
+
+The BPF verifier, prioritizing precision over analysis speed, primarily uses **Path Exploration**. When it encounters a branch, it pushes one path onto a stack and continues executing the other. It analyzes the ``true`` branch with the abstract knowledge that ``r1 > 10``, and it analyzes the ``false`` branch with the knowledge that ``r1 <= 10``.
+
+This path-sensitive approach ensures that the verifier does not falsely reject safe programs due to loss of precision, though it risks path explosion. State Pruning (Part 4) is the mechanism the verifier uses to mitigate this explosion.
+
+----
+
+Next: In **Part 2: The Abstract Domain - Values and Bounds**, we will explore how the verifier represents partial knowledge, detailing the ``tnum`` structure and numeric bounds tracking.
diff --git a/Documentation/bpf/verifier-overview-2-domain.rst b/Documentation/bpf/verifier-overview-2-domain.rst
new file mode 100644
index 000000000000..8a9d36818f24
--- /dev/null
+++ b/Documentation/bpf/verifier-overview-2-domain.rst
@@ -0,0 +1,91 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+===============================================
+Part 2: The Abstract Domain - Values and Bounds
+===============================================
+
+In Abstract Interpretation, the **Abstract Domain** defines the mathematical representation of the values a variable can hold. It determines the level of precision of the static analysis.
+
+The BPF verifier tracks several dimensions of abstract information for each register (and stack slot), encapsulated within ``struct bpf_reg_state`` (defined in ``include/linux/bpf_verifier.h``).
+
+1. The Value Lattice
+====================
+
+A lattice is a partially ordered set that models the flow of information. The lattice for the verifier represents knowledge, ranging from:
+
+* **Top ($\top$)**: The most general state. It represents *any* possible value. The verifier has zero knowledge. In the code, this is represented by the ``tnum_unknown`` bitmask and the widest possible numeric bounds (``umin_value = 0``, ``umax_value = U64_MAX``, ``smin_value = S64_MIN``, ``smax_value = S64_MAX``), applied via functions like ``__mark_reg_unknown()`` and ``__mark_reg_unbounded()``.
+* **Intermediate Values**: Partial knowledge (e.g., "the value is between 5 and 10," or "the lower 3 bits are 0").
+* **Bottom ($\bot$)**: The most specific state. It represents an impossible or contradictory state (e.g., a value that must be simultaneously > 10 and < 5). The verifier does not have an explicit ``struct`` for Bottom; instead, it manifests as contradictory bounds (e.g., ``umin_value > umax_value``). When the verifier encounters this, it identifies the execution path as dead code and stops exploring it.
+
+The goal of the verifier is to start with maximal assumptions ($\top$ for inputs) and use instructions to narrow down the possible values, moving down the lattice without ever falsely restricting the set of possible concrete executions.
+
+2. Tristate Numbers (``tnum``)
+==============================
+
+One of the most powerful abstract domains in the BPF verifier is the **Tristate Number**, implemented in ``kernel/bpf/tnum.c``.
+
+Instead of tracking precise bitwise values, a ``tnum`` tracks the state of each bit independently. Each bit can be in one of three states:
+
+1. **0**: Known to be zero.
+2. **1**: Known to be one.
+3. **u**: Unknown.
+
+A ``tnum`` is represented by two 64-bit masks: ``value`` and ``mask``.
+
+* ``value``: The bits that are known to be 1.
+* ``mask``: The bits that are unknown.
+* (Bits that are 0 in both ``value`` and ``mask`` are known to be 0).
+
+**Example:**
+
+* ``tnum_const(5)`` (Binary ``0101``): ``value = 0101``, ``mask = 0000``. All bits are known.
+* ``tnum_unknown()``: ``value = 0000``, ``mask = 1111...1111``. No bits are known ($\top$).
+* If we know a value is a multiple of 4, the lowest two bits must be zero: ``value = 0000``, ``mask = 1111...1100``.
+
+The ``tnum`` domain is exceptional for analyzing bitwise operations like AND (``&``), OR (``|``), and shifts. By tracking individual bits, the verifier can calculate the exact state of the resulting bits wherever possible, preserving a high degree of precision across bitwise operations.
+
+3. Numeric Bounds Tracking
+==========================
+
+While ``tnum`` is excellent for bitwise logic, it is imprecise for arithmetic bounds. For example, knowing a value is "less than 10" is difficult to express cleanly with a bitmask.
+
+To solve this, ``struct bpf_reg_state`` also tracks numeric bounds:
+
+* **Unsigned Bounds**: ``umin_value`` and ``umax_value``.
+* **Signed Bounds**: ``smin_value`` and ``smax_value``.
+* **32-bit Subregister Bounds**: ``u32_min_value``, ``u32_max_value``, ``s32_min_value``, ``s32_max_value``.
+
+When the verifier analyzes an instruction, it updates *both* the ``tnum`` and the numeric bounds. Furthermore, it synchronizes them. If the ``tnum`` dictates the sign bit must be 0, the verifier can update the signed bounds to be positive. If the numeric bounds dictate the maximum value is 7, the verifier can update the ``tnum`` mask to clear bits higher than 2.
+
+4. Pointer Types and Provenance
+===============================
+
+Scalars (integers) are only one part of the abstract domain. A critical security function of the verifier is distinguishing raw scalars from **Pointers**.
+
+In ``enum bpf_reg_type``, the verifier tracks the *provenance* (the origin) of pointers. This defines what the pointer fundamentally points to:
+
+* **``SCALAR_VALUE``**: A raw integer. Safe for math, unsafe for memory access.
+* **``PTR_TO_CTX``**: A pointer to the BPF context (e.g., ``struct __sk_buff``).
+* **``PTR_TO_MAP_VALUE``**: A pointer to an element within a BPF map.
+* **``PTR_TO_STACK``**: A pointer to the program's local stack.
+* **``PTR_TO_PACKET``**: A pointer to the raw network packet data.
+
+**Type Modifiers (Permissions and Safety):**
+
+Beyond the base type, the verifier enriches pointer states using bitwise modifiers defined in ``enum bpf_type_flag``. These flags act as a strict type system enforcing access permissions and safe usage contexts. Important modifiers include:
+
+* **``PTR_MAYBE_NULL``**: Indicates the pointer might be null. The verifier will aggressively reject any attempt to dereference this pointer until the program explicitly checks it against 0 (which triggers a state split, converting it to a valid pointer on the non-null path).
+* **``MEM_RDONLY``**: Denotes that the memory region the pointer references is strictly read-only.
+* **``PTR_TRUSTED``**: A vital security flag indicating the pointer was passed directly from the kernel in a safe context and is guaranteed to be valid. It is safe to pass to BPF helpers. Conversely, **``PTR_UNTRUSTED``** means the pointer was obtained by walking a chain of structs and might be invalid, restricting its use to direct, fault-handled dereferencing.
+* **``MEM_RCU``**: Indicates the memory access requires an active RCU read lock.
+
+When a register holds a pointer, the verifier conceptually separates its state into:
+
+1. **The Base Pointer**: The origin (e.g., the start of the map value) combined with its type and modifier flags.
+2. **The Offset**: The distance from the base. This offset is tracked using the scalar abstract domain (``tnum`` + bounds) described above.
+
+By separating the base and the offset, the verifier can formally prove memory safety: it ensures that for all possible values of the offset (evaluated against the scalar bounds), the resulting memory address never falls outside the allocated boundaries of the Base Pointer.
+
+----
+
+Next: In **Part 3: Data Flow and Transfer Functions**, we will explore how instructions mutate this abstract state, detailing ALU operations and conditional jumps.
diff --git a/Documentation/bpf/verifier-overview-3-dataflow.rst b/Documentation/bpf/verifier-overview-3-dataflow.rst
new file mode 100644
index 000000000000..1c7a05b46693
--- /dev/null
+++ b/Documentation/bpf/verifier-overview-3-dataflow.rst
@@ -0,0 +1,83 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+========================================
+Part 3: Data Flow and Transfer Functions
+========================================
+
+In Programming Language (PL) theory, a **Transfer Function** describes how an abstract state transitions from one state to another when an instruction is processed by the verifier.
+
+For the BPF verifier, the transfer functions map an input ``struct bpf_verifier_state`` to a new output state. This step-by-step symbolic evaluation of bytecode over the abstract domain (Part 2) is the core of the BPF verifier's safety proof.
+
+**Code Organization:**
+In the verifier's implementation, a "transfer function" is rarely a single monolithic C function. Because the abstract state consists of multiple domains (numeric bounds, bitwise ``tnum``, pointer provenance), the transfer function for a single instruction is carried out by invoking a specific operation for *each* domain. For example, when processing an addition instruction, the verifier will call ``scalar_min_max_add()`` to transform the bounds domain, and separately call ``tnum_add()`` to transform the bitwise domain, before finally synchronizing them.
+
+1. Transfer Functions for ALU Operations
+========================================
+
+Arithmetic and Logic Unit (ALU) operations (e.g., addition, subtraction, bitwise shifts) are analyzed using transfer functions that independently update the ``tnum`` state and the numeric bounds state for the destination register.
+
+The kernel implements these transfer functions in ``adjust_scalar_min_max_vals()`` (within ``kernel/bpf/verifier.c``).
+
+* **Bitwise Operations (AND, OR, XOR)**: These are highly precise in the ``tnum`` domain. For example, in an AND operation, if a bit is known to be 0 in *either* operand, the verifier can conclude the resulting bit is 0. If bits are unknown, the resulting bit is unknown.
+* **Arithmetic Operations (ADD, SUB)**: These operations naturally update the minimum and maximum boundaries (e.g., if ``r1`` is ``[2, 5]`` and ``r2`` is ``[10, 20]``, the transfer function for ``r1 += r2`` evaluates to ``[12, 25]``). Crucially, they **also update the ``tnum`` state**. The verifier uses sophisticated bitwise arithmetic in ``tnum_add()`` and ``tnum_sub()`` to track potential carry propagation, ensuring that knowledge about specific bits (like whether a value is even or a multiple of 4) is preserved even through addition and subtraction.
+
+**Handling Overflow (Loss of Precision):**
+The verifier explicitly checks for potential integer overflow or underflow during arithmetic (using functions like ``check_add_overflow()``). If an operation could result in an overflow, the verifier handles it by **widening** the abstract bounds to their maximum range (e.g., resetting ``umin`` to 0 and ``umax`` to ``U64_MAX``). This represents a "loss of precision" in the abstract domain: the verifier no longer knows the exact range of the result and must assume the most conservative state ($\top$) to remain sound. If such an unbounded value is later used as a memory offset, the verifier will reject the program.
+
+**Synchronizing Domains:**
+Because the verifier uses two parallel abstract domains (``tnum`` for bits, min/max for bounds), the ALU transfer function must synthesize them. After an ADD operation, the verifier calls ``__update_reg_bounds()``, which forces consistency:
+
+* If the numeric bounds determine a value is exactly `7`, the `tnum` is set to `value=7, mask=0`.
+* If the `tnum` shows the sign bit is 0, the signed min bound is bumped up to 0 (if it was previously negative).
+
+2. Transfer Functions for Pointers
+==================================
+
+When an ALU operation involves a pointer (e.g., ``r1 += r2``, where ``r1`` is a ``PTR_TO_MAP_VALUE`` and ``r2`` is a ``SCALAR_VALUE``), the verifier must handle it differently.
+
+This is processed in ``adjust_ptr_min_max_vals()``. The transfer function calculates how the addition of the scalar affects the allowed bounds of the pointer.
+
+* The verifier checks if the resulting abstract offset exceeds the allocated size of the memory region (e.g., the map value size).
+* To prevent speculative execution attacks (Spectre v1), the verifier may also inject runtime mitigations (masking operations) into the bytecode, depending on the abstract bounds it calculated.
+
+3. Branching and Path Exploration
+=================================
+
+The most complex transfer functions occur during control flow operations (jumps). Conditional jumps (e.g., ``if (r1 < 10) goto X``) are where the BPF verifier refines its knowledge.
+
+When the verifier evaluates a conditional branch, the abstract state splits. It creates two separate execution paths:
+
+1. **The Fall-Through Path (False Branch)**: The instruction following the jump.
+2. **The Target Path (True Branch)**: The destination instruction of the jump.
+
+The transfer function for the jump instruction refines the abstract state on *both* paths independently. This logic lives in ``check_cond_jmp_op()`` and ``reg_set_min_max()``.
+
+**Example:**
+Assume ``r1`` is an unknown scalar (``[0, U64_MAX]``). The instruction is ``if (r1 < 10) goto A; else goto B;``.
+
+* **Path A (True Branch)**: The verifier updates the abstract state for ``r1``. Since the condition was true, the new upper bound of ``r1`` is 9. The new state for ``r1`` is ``[0, 9]``.
+* **Path B (False Branch)**: The verifier updates the abstract state for ``r1``. Since the condition was false, the new lower bound of ``r1`` is 10. The new state for ``r1`` is ``[10, U64_MAX]``.
+
+By splitting the state, the verifier gains precision. It "learns" from conditionals, ensuring that subsequent memory accesses bounded by ``r1`` are proven safe on Path A, even if they would be out-of-bounds on Path B.
+
+4. Memory Access Verification
+=============================
+
+Memory access instructions (loads and stores) are validated to ensure they only read or write within permitted boundaries. The transfer function for these instructions not only updates the abstract state but also determines whether the memory access is safe, rejecting the program if bounds cannot be proven.
+
+When executing ``r2 = *(u32 *)(r1 + 0)`` (in ``check_mem_access()``), the verifier performs the following checks:
+
+1. **Provenance Check**: Is ``r1`` a valid pointer type (e.g., ``PTR_TO_MAP_VALUE``)? If it's a scalar, the verifier rejects the program.
+2. **Bounds Check**: Does the abstract offset of ``r1`` (which is a range of possible values, ``[umin, umax]``) plus the access size (4 bytes for ``u32``) fall completely within the boundaries of the memory region?
+
+   * The verifier checks the maximum possible offset. If it exceeds the boundary, the program is rejected.
+   * The verifier checks the minimum possible offset. If it is negative, the program is rejected.
+
+3. **Type Update**: After verifying the access, the transfer function updates the destination register (``r2``). The new type is determined by the metadata of the memory being accessed:
+    * **Map Values**: Typically results in a ``SCALAR_VALUE`` (unless loading a special kernel pointer/kptr).
+    * **Context (``PTR_TO_CTX``)**: The resulting type (e.g., a scalar or a ``PTR_TO_PACKET``) is determined by the specific field being read, as defined in the program type's context definition (e.g., ``struct __sk_buff``).
+    * **BTF-backed memory**: If the memory is described by BTF (see Part 5), the load results in the exact type defined in the kernel's C code (e.g., another ``PTR_TO_BTF_ID`` if reading a struct pointer).
+
+----
+
+Next: In **Part 4: State Pruning and Loop Analysis**, we will see how the verifier prevents the explosion of execution paths using state equivalence and bounded loops.
diff --git a/Documentation/bpf/verifier-overview-4-pruning.rst b/Documentation/bpf/verifier-overview-4-pruning.rst
new file mode 100644
index 000000000000..f1515011d721
--- /dev/null
+++ b/Documentation/bpf/verifier-overview-4-pruning.rst
@@ -0,0 +1,59 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+========================================
+Part 4: State Pruning and Loop Analysis
+========================================
+
+Because the BPF verifier relies on path exploration (splitting states at every branch), a naive implementation would suffer from exponential path explosion. To keep verification times reasonable—and to allow loops—the verifier employs **State Pruning**.
+
+In the context of Abstract Interpretation, pruning is conceptually related to identifying fixed points and utilizing partial ordering between abstract states.
+
+1. State Equivalence (``states_equal``)
+=======================================
+
+Before the verifier evaluates an instruction, it checks if it has been here before. It maintains a history of previously verified states at various jump targets.
+
+When the verifier reaches an instruction with a *current state*, it compares it against a *previously verified state* (an *existing state*) at the same instruction.
+
+This comparison is performed by ``states_equal()`` (in ``kernel/bpf/verifier.c``). Crucially, ``states_equal`` is *not* a strict equality check. It is a **subsumption** (or partial order) check.
+
+It asks: *Is the current state "more specific" than (or equal to) the existing state?*
+
+If the *current state* is subsumed by the *existing state*, it means every possible concrete execution represented by the current state is a subset of the executions already proven safe by the existing state. Therefore, the verifier can safely **prune** the current path. It stops evaluating the *current state* and marks the branch as safe.
+
+**Examples of Subsumption:**
+
+* If the *existing state* had a register as $\top$ (completely unknown scalar) and the *current state* has that same register bounded between 5 and 10, then the current state is subsumed. The existing state proved safety for *any* value, so a restricted value is naturally safe.
+* If both the *existing state* and the *current state* have a register as a ``PTR_TO_MAP_VALUE`` with the same offset, they are equal, so it's safe to prune.
+* If the *existing state* had a register bounded between 5 and 10, but the *current state* has it bounded between 0 and 15, the *current state* is *wider*. It is not subsumed. The verifier must continue evaluating the *current state*.
+
+2. Liveness Tracking (Dead State Elimination)
+=============================================
+
+To maximize pruning, the verifier uses **Liveness Analysis** (a classic data-flow analysis technique). If a register's value is never read before being overwritten on a path, it is "dead."
+
+The verifier performs this liveness analysis in a separate pass (``compute_live_registers()``) before the main path exploration (``do_check()``) begins. By analyzing the program's control flow in advance, the verifier pre-determines which registers are dead at any given instruction.
+
+The verifier tracks this using ``REG_LIVE_READ`` and ``REG_LIVE_WRITTEN`` flags. During the ``states_equal()`` check, if a register is marked as dead in the *existing state*, the verifier knows that this register will remain dead regardless of how the current path is explored. As a result, it completely ignores the value of that register in the *current state*.
+
+By ignoring dead registers, the verifier increases the probability that a *current state* is subsumed by an *existing state*, leading to higher pruning rates and faster verification.
+
+3. Loop Verification (Bounded Loops)
+====================================
+
+Historically, BPF programs had to be Directed Acyclic Graphs (DAGs). Any back-edge (a jump to an ancestor in the Control Flow Graph) was instantly rejected to guarantee termination.
+
+Modern BPF supports **Bounded Loops** (``bpf_loop`` helper or direct `goto` back-edges under specific conditions).
+
+To verify a loop without infinite analysis, the verifier relies on a form of **Bounded Abstract Interpretation** and **Widening**.
+
+1. **Loop State Generation**: When a back-edge is taken, the verifier evaluates the loop body multiple times.
+2. **State Convergence**: On each iteration, the abstract state at the loop header is updated. Variables modified in the loop (e.g., induction variables like ``i = i + 1``) will have their bounds grow.
+3. **Termination Proof**: The verifier must prove that the loop induction variable eventually reaches the loop exit condition. If ``i`` is bounded by a constant, and the loop exits when ``i >= MAX``, the verifier can track the maximum bound of ``i``.
+4. **State Equivalence in Loops**: If the abstract state at the loop header converges (i.e., iterating the loop no longer widens the abstract bounds, or the new state is subsumed by a previous iteration's state), the verifier has found a safe fixed-point and can prune the loop exploration.
+
+If the verifier cannot prove that a loop terminates (e.g., the upper bound of the induction variable relies on data read from memory rather than a known scalar), or if it hits the maximum instruction complexity limit (historically 1 million simulated instructions), it rejects the program.
+
+----
+
+Next: In **Part 5: Advanced Contexts - Concurrency and BTF**, we will explore how the verifier handles modern extensions like the BPF Type Format, spinlocks, and subprogram analysis.
diff --git a/Documentation/bpf/verifier-overview-5-advanced.rst b/Documentation/bpf/verifier-overview-5-advanced.rst
new file mode 100644
index 000000000000..f18d13dd8cab
--- /dev/null
+++ b/Documentation/bpf/verifier-overview-5-advanced.rst
@@ -0,0 +1,70 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+===============================================
+Part 5: Advanced Contexts - Concurrency and BTF
+===============================================
+
+As BPF evolved from simple packet filtering into a complex subsystem capable of replacing kernel modules (e.g., tracing, LSMs, XDP), the verifier's abstract interpretation framework had to expand.
+
+1. BPF Type Format (BTF) and Introspection
+==========================================
+
+The :doc:`btf` is a metadata format that provides full C-language type information for kernel structures. Within the verifier's abstract interpretation framework, BTF acts as a static type system.
+
+**BTF Availability:**
+
+BTF type information is not always available. Its presence depends on:
+
+* **Kernel Configuration**: The kernel must be compiled with ``CONFIG_DEBUG_INFO_BTF=y`` to provide introspection for its own internal types.
+* **Program Metadata**: BPF programs themselves can optionally include BTF data to describe their own structures (e.g., map values).
+* **Verifier Context**: When BTF is unavailable, the verifier falls back to more coarse-grained checks based purely on memory region boundaries (as described in Part 2).
+
+**Type-Aware Abstract Domains:**
+
+When BTF is enabled and the program traces a kernel function to receive a pointer (e.g., ``struct task_struct *task``), the verifier marks the register with the type ``PTR_TO_BTF_ID``.
+
+* The ``btf_id`` points to the formal type definition in the kernel's BTF metadata.
+* When the program executes ``r2 = *(u64 *)(r1 + offsetof(task, pid))``, the verifier doesn't just do numeric bounds checking. It performs **Type Checking**.
+* The transfer function looks up the ``btf_id`` for ``struct task_struct``, finds the field at the requested offset, checks its size (e.g., a 4-byte integer), and checks its type.
+* The destination register (``r2``) is then updated. If the field was an integer, ``r2`` becomes a ``SCALAR_VALUE``. If the field was a pointer to another struct (e.g., ``task->real_parent``), ``r2`` becomes a new ``PTR_TO_BTF_ID`` representing that parent struct.
+
+This allows BPF programs to traverse arbitrary kernel data structures with compile-time safety guarantees, directly mirroring the type checking performed by the C compiler.
+
+2. Concurrency Analysis (Spinlocks and RCU)
+===========================================
+
+BPF programs can run concurrently on multiple CPUs. The verifier must analyze code for data races and illegal lock usage, effectively enforcing **Lock State Tracking**.
+
+**The Abstract Lock State:**
+
+The ``struct bpf_verifier_state`` includes fields like ``active_spin_lock`` and ``active_rcu_lock``.
+
+* **Spinlocks**: When a program calls the helper ``bpf_spin_lock(map_value)``, the verifier's transfer function asserts that no lock is currently held. It then updates ``active_spin_lock`` with the identity of the map value.
+* The verifier ensures that while a spinlock is held, the program cannot sleep (e.g., calling certain blocking helpers) and cannot return without releasing it (``bpf_spin_unlock``).
+* **RCU Sections**: For tracing and memory traversal, BPF uses RCU. The ``active_rcu_lock`` counter tracks the nesting depth of ``bpf_rcu_read_lock()`` calls. The verifier ensures that RCU pointers (tagged with ``MEM_RCU``) are only dereferenced when the RCU read lock is actively held.
+
+By making lock status an explicit part of the abstract state, the verifier statically proves the absence of deadlocks and use-after-free bugs related to concurrency.
+
+3. Resource Lifecycle and Reference Tracking
+============================================
+
+For complex programs that allocate kernel resources (e.g., performing a socket lookup via ``bpf_sk_lookup_tcp``), the verifier enforces a strict **Acquire-Release** lifecycle. This ensures that every allocated resource is either released or appropriately handled before the program terminates.
+
+In the language of Abstract Interpretation, this is implemented by extending the abstract state with a **Reference Tracking** domain.
+
+* **Acquisition (KF_ACQUIRE)**: When the verifier executes a transfer function for an "acquire" helper or kfunc, it generates a unique ``ref_obj_id``. A new entry is added to the ``refs`` array within ``struct bpf_verifier_state``, and the return register (``r0``) is tagged with this ID.
+* **Reference Propagation**: The ``ref_obj_id`` is part of the register's abstract state. If the program copies the pointer to another register or spills it to the stack, the ID follows it.
+* **Release (KF_RELEASE)**: When a "release" function (e.g., ``bpf_sk_release``) is called, the verifier matches the ``ref_obj_id`` of the argument. It then removes the reference from the abstract state's ``refs`` array and **invalidates** all other registers or stack slots sharing that same ID, preventing use-after-free errors.
+* **Termination Proof**: At the ``BPF_EXIT`` instruction, the verifier asserts that the ``refs`` array is empty. If any reference remains, the program is rejected as it has "leaked" a kernel resource.
+
+4. Inter-Procedural Analysis (Subprograms)
+==========================================
+
+BPF supports subprograms (calling local BPF functions using ``bpf_call``). Unlike simple inlining, the verifier performs true **Inter-Procedural Analysis (IPA)**.
+
+1. **Call Frame Management**: When a ``bpf_call`` occurs, the verifier pushes a new call frame onto its abstract state. The caller's registers (``r6``-``r9``, which are callee-saved) are preserved in the caller's frame.
+2. **Argument Passing**: The arguments (``r1``-``r5``) are passed from the caller to the callee. The verifier enforces that these arguments match the expected types (which it deduces during an initial pass).
+3. **Stack Depth Validation**: The verifier computes the total stack size used by a function and its callees to ensure it never exceeds the strict 512-byte limit.
+4. **Return Value Tracking**: When the callee hits the ``BPF_EXIT`` instruction, the verifier updates the caller's ``r0`` with the abstract state of the return value, pops the call frame, and resumes exploration in the caller.
+
+By modeling the full call stack in the abstract state, the verifier ensures that function boundaries do not compromise safety.
diff --git a/Documentation/bpf/verifier-overview-index.rst b/Documentation/bpf/verifier-overview-index.rst
new file mode 100644
index 000000000000..3d5bffd98767
--- /dev/null
+++ b/Documentation/bpf/verifier-overview-index.rst
@@ -0,0 +1,17 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+============================
+Overview of the BPF Verifier
+============================
+
+This is an index to multi-part documentation that gives an overview of the
+eBPF verifier.
+
+.. toctree::
+   :maxdepth: 2
+
+   verifier-overview-1-abstr-interp
+   verifier-overview-2-domain
+   verifier-overview-3-dataflow
+   verifier-overview-4-pruning
+   verifier-overview-5-advanced
-- 
2.53.0.473.g4a7958ca14-goog

Re: [RFC PATCH 1/1] bpf, docs: structured docs for the verifier

[bot+bpf-ci]

[-- Attachment #1: Type: text/plain, Size: 3977 bytes --]

> Multi-part docseries (verifier-formal-*.rst) for BPF verifier.

The files are named verifier-overview-*.rst, not
verifier-formal-*.rst.

> diff --git a/Documentation/bpf/verifier-overview-2-domain.rst b/Documentation/bpf/verifier-overview-2-domain.rst
> new file mode 100644
> index 000000000000..8a9d36818f24
> --- /dev/null
> +++ b/Documentation/bpf/verifier-overview-2-domain.rst

[ ... ]

> +* **Top ($\top$)**: The most general state. It represents *any* possible value. The verifier has zero knowledge. In the code, this is represented by the ``tnum_unknown`` bitmask and the widest possible numeric bounds (``umin_value = 0``, ``umax_value = U64_MAX``, ``smin_value = S64_MIN``, ``smax_value = S64_MAX``), applied via functions like ``__mark_reg_unknown()`` and ``__mark_reg_unbounded()``.
> +* **Intermediate Values**: Partial knowledge (e.g., "the value is between 5 and 10," or "the lower 3 bits are 0").
> +* **Bottom ($\bot$)**: The most specific state. It represents an impossible or contradictory state (e.g., a value that must be simultaneously > 10 and < 5). The verifier does not have an explicit ``struct`` for Bottom; instead, it manifests as contradictory bounds (e.g., ``umin_value > umax_value``). When the verifier encounters this, it identifies the execution path as dead code and stops exploring it.

The $\top$ and $\bot$ LaTeX notations will not render in Sphinx
RST. The kernel documentation build uses Sphinx with mathjax as
the math renderer, but dollar-sign delimiters are not enabled by
default. These will appear literally as "$\top$" and "$\bot$" in
the generated HTML.

The standard RST inline math syntax would be :math:`\top` and
:math:`\bot`. The same issue appears in a few other places across
Parts 2, 3, and 4 (e.g. the $\top$ in the tnum_unknown example
and in Part 3's overflow section and Part 4's subsumption
examples).

> diff --git a/Documentation/bpf/verifier-overview-4-pruning.rst b/Documentation/bpf/verifier-overview-4-pruning.rst
> new file mode 100644
> index 000000000000..f1515011d721
> --- /dev/null
> +++ b/Documentation/bpf/verifier-overview-4-pruning.rst

[ ... ]

> +The verifier tracks this using ``REG_LIVE_READ`` and ``REG_LIVE_WRITTEN`` flags. During the ``states_equal()`` check, if a register is marked as dead in the *existing state*, the verifier knows that this register will remain dead regardless of how the current path is explored. As a result, it completely ignores the value of that register in the *current state*.

REG_LIVE_READ and REG_LIVE_WRITTEN do not exist anywhere in the
current kernel tree. The actual liveness mechanism is implemented
in compute_live_registers(), which uses bitmask-based
insn_live_regs structs with in/out/use/def fields, and stores the
results as insn_aux[i].live_regs_before.

Could these references be updated to describe the actual
implementation?

> diff --git a/Documentation/bpf/verifier-overview-5-advanced.rst b/Documentation/bpf/verifier-overview-5-advanced.rst
> new file mode 100644
> index 000000000000..f18d13dd8cab
> --- /dev/null
> +++ b/Documentation/bpf/verifier-overview-5-advanced.rst

[ ... ]

> +The ``struct bpf_verifier_state`` includes fields like ``active_spin_lock`` and ``active_rcu_lock``.
> +
> +* **Spinlocks**: When a program calls the helper ``bpf_spin_lock(map_value)``, the verifier's transfer function asserts that no lock is currently held. It then updates ``active_spin_lock`` with the identity of the map value.

The field active_spin_lock does not exist in struct
bpf_verifier_state. The actual fields are active_locks (u32),
active_lock_id (u32), and active_lock_ptr (void *).

Similarly, active_rcu_lock should be active_rcu_locks (plural) to
match the actual field name in the struct.


---
AI reviewed your patch. Please fix the bug or email reply why it's not a bug.
See: https://github.com/kernel-patches/vmtest/blob/master/ci/claude/README.md

CI run summary: https://github.com/kernel-patches/bpf/actions/runs/22853419607

Re: [RFC PATCH 1/1] bpf, docs: structured docs for the verifier

[Alexei Starovoitov]

On Mon, Mar 9, 2026 at 5:10 AM Burak Emir <bqe@google.com> wrote:
>
> Multi-part docseries (verifier-formal-*.rst) for BPF verifier.
>
> Provides some background that helps get a structured overview of
> the static analysis that happens in the verifier.
>
> The documentation covers:
> * Part 1: Abstract Interpretation
> * Part 2: Abstract Domain (Value lattices, tnum, pointer provenance)
> * Part 3: Data Flow (Transfer functions, ALU ops, bounds tracking)
> * Part 4: Pruning (State equivalence, subsumption, liveness)
> * Part 5: Advanced Contexts (BTF, concurrency, reference tracking)
>
> Signed-off-by: Burak Emir <bqe@google.com>
> Assisted-by: Gemini:gemini-3.1-pro,gemini-3-flash

Pls don't waste the maintainer's time with this.

pw-bot: cr