[PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement

[PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement

[Hao Sun]

This patch set (and three follow-up sets) introduces a proof-based, on-demand
refinement mechanism that increases verifier precision while keeping kernel
complexity bounded. The kernel performs lightweight symbolic tracking and state
updates; userspace does the heavy reasoning and returns a proof, which the
kernel checks.

The design is named as BCF: eBPF Certificate Framework.

Motivation
----------

The eBPF verifier can reject safe programs due to imprecise techniques used,
e.g., intervals, that do not track registers relations and over-approximate
on each step. This leads to rejections from loose bounds and infeasible paths.
The dataset[1] shows various concrete false rejections. In practice, they
require non-trivial refactoring and trial-and-error to mitigate, due to the
gap between bytecode errors and high-level code. Cases inside deep loops and
long paths are particularly challenging.

With the increasing adoption of eBPF in various subsystems, a more powerful
verifier is beneficial, to allow more complex extensions to be verified as
well as being transparent to the user.

The goal is to accept more safe programs without turning the verifier into
an SMT solver or significantly increasing kernel complexity: leverage
solver-grade reasoning (500k+ LOC solvers) without trusting it, by
checking compact proofs in a ~5k LOC in-kernel proof checker.

Key design
----------

The patch sets introduce proof-based, on-demand verifier state refinement.
On a blocking check (e.g., potential OOB), the verifier performs on-demand
refinement:

1. Backtrack the target register to identify the relevant path suffix.
2. Symbolically track the suffix to collect precise bitvector/boolean
   expressions for involved registers and the path condition.
3. Derive a refinement condition (SMT) that, if valid, permits the verifier to
   continue (e.g., tighten pointer offset or size bounds, or conclude the path
   is unreachable).
4. Send the condition to userspace. Userspace proves it and returns a proof.
5. The kernel checks the proof and resumes analysis with the refined state.

Only lightweight work is in-kernel: suffix tracking and proof checking. The
NP-hard reasoning remains in userspace. More details can be found in our
research paper[5] (received the best paper award :).

It's highly recomended to play with the system directly: (1) apply all
the patches from our repo[4], (2) download the provided disk image,
and (3) see how the verifier, proof checker, loader, and solver interact
with each other via loading the example programs provided[6].

Here is a running example:

A simplified load log that hits an infeasible branch; refinement proves the path
unreachable and pops it (another example is also available in our paper).

The verifier starts:
```
0: (85) call bpf_get_prandom_u32#7    ; R0=scalar()
1: (bc) w1 = w0                       ; R0=scalar() R1=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
2: (c4) w1 s>>= 31                    ; R1=scalar(smin=0,smax=umax=0xffffffff,smin32=-1,smax32=0,var_off=(0x0; 0xffffffff))
3: (54) w1 &= -134                    ; R1=scalar(smin=0,smax=umax=umax32=0xffffff7a,smax32=0x7fffff7a,var_off=(0x0; 0xffffff7a))
4: (66) if w1 s> 0xffffffff goto pc+2 ; R1=scalar(smin=umin=umin32=0x80000000,smax=umax=umax32=0xffffff7a,smax32=-134,var_off=(0x80000000; 0x7fffff7a))
5: (56) if w1 != 0xffffff78 goto pc+1 ; R1=0xffffff78
6: (bf) r1 = r2
R2 !read_ok            ; ---> start refinement: prove the path unreachable
```

Symbolic tracking (on the suffix):
```
...
1: (bc) w1 = w0                 ; w1 = sym
2: (c4) w1 s>>= 31              ; w1 = (sym s>> 31)
3: (54) w1 &= -134              ; w1 = (sym s>> 31) & -134
4: (66) if w1 s> -1 goto pc+2   ; fallthrough c1: w1 s<= -1
5: (56) if w1 != -136 goto pc+1 ; fallthrough c2: w1 = -136
6: (bf) r1 = r2
```

Here, `sym` refers to a 32-bit bitvector, which represents a vector of
unknown bits (in the same spirit as tnum); however, unlike the verifier,
the symbolic tracking does not perform any "reasoning": it simply
records all the computation as is:
	{src=sym0, dst=sym1} dst op= src {dst = (sym1 op sym0)},
each calculation is captured as a symbolic expression (in comparison,
tnum needs to approximate at every step).

For the suffix, the symbolic track just captures the symbolic expression
for each reg, and for branch conditions, it remembers the condition as
path constraints (the AND of each taken condition).

For the example above, let t = (sym s>> 31) & -134, which is the associated
expr to w1. The condition to refute is:
	 t <= -1 && t == -136
It does not hold (if t s<= -1, then t must be -134), hence the path is
unreachable. This condition is sent to user space for a proof.

In user space, the condition is translated into the following SMT formula:
```
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 64))
(assert (let ((t20 (bvand (bvashr ((_ extract 31 0) v0) (_ bv31 32)) (_ bv4294967162 32))))
        (and (bvsle t20 (_ bv4294967295 32)) (= t20 (_ bv4294967160 32)))))
(check-sat)
(exit)
```

cvc5 returns `unsat` and a proof:
```
unsat
(
; Proof produced: 715 steps, 17244 bytes
)
```

Now back to the kernel space, the proof checker checks the proof:
```
checking 715 proof steps	; ---> proved received, starting checking:
(#0 POLY_NORM () ...)
(#1 POLY_NORM_EQ (@p0) ...)
(#2 REFL () ...)
(#3 ACI_NORM () ...)
(#4 ABSORB () ...)
(#5 EVALUATE () ...)
...
proof accepted            ; Path proved to be unreachable
```

The verifier pops the path and continues:
```
from 5 to 7: R0=scalar() R1=scalar(...)
; return 0; @ unreachable_arsh.bpf.c:29
7: (b7) r0 = 0                        ; R0=0
8: (95) exit

from 4 to 7: safe
processed 10 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 0
```

The proof check is a linear scan and is highly efficient, e.g., for a 8M
proof, the checker can validate it within 3s.

In summary, the linear time proof check essentially allows the verifier
to achieve various non-trivial refinements, by using the user space SMT
solvers but not trust them.

Kernel/userspace interface and workflow
---------------------------------------

UAPI carries refinement conditions, proofs, and an anon-fd to preserve the
verifier env across proof requests:

- union bpf_attr: `bcf_buf`, `bcf_buf_size`, `bcf_buf_true_size`, `bcf_fd`,
  `bcf_flags` (`BCF_F_PROOF_REQUESTED`, `BCF_F_PROOF_PROVIDED`,
  `BCF_F_PROOF_PATH_UNREACHABLE`).
- Conditions and proofs are represented as `struct bcf_expr` and `struct
  bcf_proof_step`.

The condition and proof are DAG, the associated algorithms walk them.

Workflow:
- Initial verification may request a proof and return `bcf_fd` plus the
  expression arena and condition.
- Userspace (bpftool + cvc5) proves the condition and resubmits with
  `BCF_F_PROOF_PROVIDED` and the proof in `bcf_buf`.
- Resume: the kernel validates the proof and continues from the saved state.

More on the proof checker
-------------------------

A proof checker validates that a sequence of proof rule applications
proves a required goal. Given a goal and a proof (a list of rule
applications), the checker verifies each rule is applied exactly in its
permitted form and that the final conclusion matches the requested goal;
any violation leads to proof rejection. For example, from premises
`A and B`, the AND_ELIM rule may conclude `A` (or `B`) only; otherwise
the checker rejects it.

The checker enforces rule validity and goal consistency, enabling
trustless validation: user space may reason a formula, but the kernel
only accepts results backed by a proof that checks.

The proof checker introduced in this patch set can also be executed in
*user space*, with all dependent kernel routines stubbed with their
user-space counterparts. One can compile and try it with the proofs
in our repo[6], and see the proof checking process.

Proof checker complexity
------------------------

The cost/complexity is mostly the checker itself. The proof checker
as introduced in the previous section is essentially a linear scan of
the given proof. While our patch sets are a bit huge and the checker
contains about 5k lines of code, its complexity is much lower than
the verifier.

Comparisons to the verifier:

The complexity of the verifier is non-linear in the sense that every
time when one wants to extend the verifier, e.g., adding a field to
the verifier_state struct, a lot of factors need to be considered:
(1) the effects of every instruction on this field, (2) its semantics
for state pruning, (3) liveness/precision potentially kick in, etc.

In comparison, the proof checker is a **linear** combination of a fixed
set of proof rules:
    - They are independent of each other:
    - Adding a new rule does not break other rules;
    - Understanding one rule does not require understanding other rules.
The complexity is essentially the sum of the complexity of each rule.

Most rules are relatively straightforward (see boolean rules), while
only a few require a bit more thinking; these essentially include
two classes of rules: rewrite and bitblast.

The overall workflow of the checker is just a while loop that scans
each rule (see apply_rules()), while in comparison, the verifier is
a DFS over the program's CFG.

The proof checker is quite stable: (1) in theory, it only needs
to support two rules, resolution and bitblast, to be complete to
represent any proof; (2) in practice, the checker supports tens
of other rules to reduce proof size; (3) the supported rules are
stable and do not require frequent changes, except for some rewrites.

This makes the checker easier to maintain then the verifier.
Currently supporte 50 rules in total:
	core   : 14
	boolean: 33
	bitvec : 3

Additional benefits
-------------------

Beyond refinement, the checker can validate other non-trivial facts,
one potential use is to validate the precomputed loop fixpoints
(state sets) to simplify the verifier (outlined here; future work).

Current cost of loop analysis: kernel must compute fixpoints at
loop/join points, causing state explosion and complexity when
combined with liveness/precision tracking.

Proof-enabled design: User space provides fixpoint in-states for
loop entries and join points; the kernel validates the provided
fixpoint instead of compute by itself.

Refined verifier algorithm (single pass):
- Userspace input:
  - For each basic block bb, a finite set S_in[bb] describing a fixpoint
    in-state at bb, i.e., the set of states that can be reached from bb.

1. For each bb, take S_in[bb] as incoming states.
2. Analayze the bb once per incoming state to compute S_out for
   each successor (validation phase).
3. For each edge bb->succ, check inclusion S_out[bb->succ] \in S_in[succ].
   If non-trivial, i.e., the verifier cannot verify, emit a containment
   formula G and request a proof; the check then validates the proof.
4. Accept if all inclusions are validated. This witnesses a state
   fixpoint; no kernel-side iteration is needed.

This potentially enables smaller state sets computed offline, reducing
the number of states required to analyze. The wholse analysis is a linear
scan, no liveness/precision track, and the proof is only basic block-wise.

Correctness and evaluation
--------------------------

We validated the checker and enhanced verifier on benchmarks: programs[1] and
formulas[2] with cvc5 proofs. Proof sizes range from 168 bytes to 8.4 MB; the
largest validate in under ~3 seconds. Sanitizers report no memory errors. With
this enhancement, 403 of 512 previously rejected programs can be verified. The
precision is comparable to symbolic-execution-based approaches, while keeping
kernel complexity low.

Patch set contents (this set)
-----------------------------

This set adds the initial proof checker and the verifier refinement workflow,
and it targets `bpf-next`:

  - Patches 1–2: UAPI expression/proof definitions and checker skeleton.
  - Patch 3: UAPI for condition/proof interaction (`bcf_*` fields and flags).
  - Patch 4: High-level `bcf_refine()` and backtracking logic.
  - Patches 5–13: Symbolic tracking (suffix matching, expr arena, MOV/SEXT,
    scalar/pointer ALU with 32-bit lowering, spill/fill, path constraints) and
    pruning controls for parent states.
  - Patch 14: Refinements: path-unreachable and memory-access bound refinement
    (ptr offset and size tightening, var/var safe-access marking).
  - Patches 15–16: Preserve env, request proof, resume and check proof.
  - Patch 17: Enable BCF for privileged users (`bcf.available`).

References
----------

[1] Benchmark programs: https://github.com/SunHao-0/BCF/tree/main/bcf-progs
[2] Benchmark proofs: https://github.com/SunHao-0/BCF/tree/main/bcf-proofs
[3] Early prototype: https://github.com/SunHao-0/BCF/tree/artifact-evaluation
[4] Current full implementation: https://github.com/SunHao-0/BCF
[5] SOSP paper: https://dl.acm.org/doi/10.1145/3731569.3764796
[6] Proof checker: https://github.com/SunHao-0/BCF/tree/main/bcf-checker

Hao Sun (17):
  bpf: Add BCF expr and proof rule definitions
  bpf: Add bcf_checker top-level workflow
  bpf: Add UAPI fields for BCF proof interaction
  bpf: Add top-level workflow of bcf_refine()
  bpf: Add top-level workflow of bcf_track()
  bpf: Add bcf_match_path() to follow the path suffix
  bpf: Add bcf_expr management and binding
  bpf: Track mov and signed extension
  bpf: Track alu operations in bcf_track()
  bpf: Add bcf_alu() 32bits optimization
  bpf: Track stack spill/fill in bcf_track()
  bpf: Track path constraint
  bpf: Skip state pruning for the parent states
  bpf: Add mem access bound refinement
  bpf: Preserve verifier_env and request BCF
  bpf: Resume verifier env and check proof
  bpf: Enable bcf for priv users

 .clang-format                  |    2 +
 include/linux/bcf_checker.h    |   18 +
 include/linux/bpf.h            |    1 +
 include/linux/bpf_verifier.h   |   34 +
 include/uapi/linux/bcf.h       |  197 +++++
 include/uapi/linux/bpf.h       |   21 +
 kernel/bpf/Makefile            |    2 +-
 kernel/bpf/bcf_checker.c       |  440 ++++++++++
 kernel/bpf/liveness.c          |   15 +
 kernel/bpf/syscall.c           |   27 +-
 kernel/bpf/verifier.c          | 1397 +++++++++++++++++++++++++++++++-
 tools/include/uapi/linux/bpf.h |   21 +
 12 files changed, 2143 insertions(+), 32 deletions(-)
 create mode 100644 include/linux/bcf_checker.h
 create mode 100644 include/uapi/linux/bcf.h
 create mode 100644 kernel/bpf/bcf_checker.c

--
2.34.1

[PATCH RFC 01/17] bpf: Add BCF expr and proof rule definitions

[Hao Sun]

This patch adds include/uapi/linux/bcf.h with:

- Expression node format:
  struct bcf_expr { u8 code; u8 vlen; u16 params; u32 args[]; }
  * code encodes (operation(5 bits)| type (3 bits)). The op first reuses
    all the bpf encoding, e.g., BPF_ADD/BPF_SUB, and then, extends it
    with bitvector specific ops, e.g., extract.
  * args[] holds u32 indices into the same arena (DAG by backwards indices);
    BV VAL is the only op whose args carry immediates.
  * params packs op-specific fields; helpers are provided to access
    bit widths, extract ranges, extension sizes, boolean literal bits.

- Proof buffer layout and rule ids:
  * struct bcf_proof_header { magic=BCF_MAGIC, expr_cnt, step_cnt }.
  * struct bcf_proof_step { u16 rule; u8 premise_cnt; u8 param_cnt; u32 args[] };
    args[] is (premise ids followed by parameters).
  * Rule classes are ORed into rule (BCF_RULE_CORE/BOOL/BV).

This patch is UAPI-only; no kernel behavior change.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/uapi/linux/bcf.h | 197 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 197 insertions(+)
 create mode 100644 include/uapi/linux/bcf.h

diff --git a/include/uapi/linux/bcf.h b/include/uapi/linux/bcf.h
new file mode 100644
index 000000000000..459ad3ed5c6f
--- /dev/null
+++ b/include/uapi/linux/bcf.h
@@ -0,0 +1,197 @@
+/* SPDX-License-Identifier: GPL-2.0 WITH Linux-syscall-note */
+#ifndef _UAPI__LINUX_BCF_H__
+#define _UAPI__LINUX_BCF_H__
+
+#include <linux/types.h>
+#include <linux/bpf.h>
+
+/* Expression Types */
+#define BCF_TYPE(code)	((code) & 0x07)
+#define BCF_BV		0x00	/* Bitvector */
+#define BCF_BOOL	0x01	/* Boolean */
+#define BCF_LIST	0x02	/* List of vals */
+#define __MAX_BCF_TYPE	0x03
+
+#define BCF_OP(code)	((code) & 0xf8)
+/* Common Operations */
+#define BCF_VAL		0x08	/* Value/Constant */
+#define BCF_VAR		0x18	/* Variable */
+#define BCF_ITE		0x28	/* If-Then-Else */
+
+/* Bitvector Operations */
+#define BCF_SDIV	0xb0
+#define BCF_SMOD	0xd0
+#define BCF_EXTRACT	0x38	/* Bitvector extraction */
+#define BCF_SIGN_EXTEND	0x48	/* Sign extension */
+#define BCF_ZERO_EXTEND	0x58	/* Zero extension */
+#define BCF_BVSIZE	0x68	/* Bitvector size */
+#define BCF_BVNOT	0x78	/* Bitvector not */
+#define BCF_FROM_BOOL	0x88	/* Bool list to Bitvector */
+#define BCF_CONCAT	0x98	/* Concatenation */
+#define BCF_REPEAT	0xa8	/* Bitvector repeat */
+
+/* Boolean Operations */
+#define BCF_CONJ	0x00	/* Conjunction (AND) */
+#define BCF_DISJ	0x40	/* Disjunction (OR) */
+#define BCF_NOT		0x80	/* Negation */
+#define BCF_IMPLIES	0x90	/* Implication */
+#define BCF_XOR		0x38	/* Exclusive OR */
+#define BCF_BITOF	0x48	/* Bitvector to Boolean */
+
+/* Boolean Literals/Vals */
+#define BCF_FALSE	0x00
+#define BCF_TRUE	0x01
+
+/**
+ * struct bcf_expr - BCF expression structure
+ * @code: Operation code (operation | type)
+ * @vlen: Argument count
+ * @params: Operation parameters
+ * @args: Argument indices
+ *
+ * Parameter encoding by type:
+ * - Bitvector: [7:0] bit width, except:
+ *	- [15:8] and [7:0] extract `start` and `end` for EXTRACT;
+ *	- [15:8] repeat count for REPEAT;
+ *	- [15:8] extension size for SIGN/ZERO_EXTEND
+ * - Boolean:
+ *	- [0] literal value for constants;
+ *	- [7:0] bit index for BITOF.
+ * - List: element type encoding:
+ *	- [7:0] for types;
+ *	- [15:8] for type parameters, e.g., bit width.
+ */
+struct bcf_expr {
+	__u8	code;
+	__u8	vlen;
+	__u16	params;
+	__u32	args[];
+};
+
+#define BCF_PARAM_LOW(p)	((p) & 0xff)
+#define BCF_PARAM_HIGH(p)	(((p) >> 8) & 0xff)
+
+/* Operation-specific parameter meanings */
+#define BCF_BV_WIDTH(p)		BCF_PARAM_LOW(p)
+#define BCF_EXT_LEN(p)		BCF_PARAM_HIGH(p)
+#define BCF_EXTRACT_START(p)	BCF_PARAM_HIGH(p)
+#define BCF_EXTRACT_END(p)	BCF_PARAM_LOW(p)
+#define BCF_REPEAT_N(p)		BCF_PARAM_HIGH(p)
+#define BCF_BOOL_LITERAL(p)	((p) & 1)
+#define BCF_BITOF_BIT(p)	BCF_PARAM_LOW(p)
+#define BCF_LIST_TYPE(p)	BCF_PARAM_LOW(p)
+#define BCF_LIST_TYPE_PARAM(p)	BCF_PARAM_HIGH(p)
+
+/* BCF proof definitions */
+#define BCF_MAGIC	0x0BCF
+
+struct bcf_proof_header {
+	__u32	magic;
+	__u32	expr_cnt;
+	__u32	step_cnt;
+};
+
+/**
+ * struct bcf_proof_step - Proof step
+ * @rule: Rule identifier (class | rule)
+ * @premise_cnt: Number of premises
+ * @param_cnt: Number of parameters
+ * @args: Arguments (premises followed by parameters)
+ */
+struct bcf_proof_step {
+	__u16	rule;
+	__u8	premise_cnt;
+	__u8	param_cnt;
+	__u32	args[];
+};
+
+/* Rule Class */
+#define BCF_RULE_CLASS(r)	((r) & 0xe000)
+#define BCF_RULE_CORE		0x0000
+#define BCF_RULE_BOOL		0x2000
+#define BCF_RULE_BV		0x4000
+
+#define BCF_STEP_RULE(r)	((r) & 0x1fff)
+
+/* Core proof rules */
+#define BCF_CORE_RULES(FN)  \
+	FN(ASSUME)          \
+	FN(EVALUATE)        \
+	FN(DISTINCT_VALUES) \
+	FN(ACI_NORM)        \
+	FN(ABSORB)          \
+	FN(REWRITE)         \
+	FN(REFL)            \
+	FN(SYMM)            \
+	FN(TRANS)           \
+	FN(CONG)            \
+	FN(TRUE_INTRO)      \
+	FN(TRUE_ELIM)       \
+	FN(FALSE_INTRO)     \
+	FN(FALSE_ELIM)
+
+#define BCF_RULE_NAME(x) BCF_RULE_##x
+#define BCF_RULE_ENUM_VARIANT(x) BCF_RULE_NAME(x),
+
+enum bcf_core_rule {
+	BCF_RULE_CORE_UNSPEC = 0,
+	BCF_CORE_RULES(BCF_RULE_ENUM_VARIANT)
+	__MAX_BCF_CORE_RULES,
+};
+
+/* Boolean proof rules */
+#define BCF_BOOL_RULES(FN)   \
+	FN(RESOLUTION)       \
+	FN(FACTORING)        \
+	FN(REORDERING)       \
+	FN(SPLIT)            \
+	FN(EQ_RESOLVE)       \
+	FN(MODUS_PONENS)     \
+	FN(NOT_NOT_ELIM)     \
+	FN(CONTRA)           \
+	FN(AND_ELIM)         \
+	FN(AND_INTRO)        \
+	FN(NOT_OR_ELIM)      \
+	FN(IMPLIES_ELIM)     \
+	FN(NOT_IMPLIES_ELIM) \
+	FN(EQUIV_ELIM)       \
+	FN(NOT_EQUIV_ELIM)   \
+	FN(XOR_ELIM)         \
+	FN(NOT_XOR_ELIM)     \
+	FN(ITE_ELIM)         \
+	FN(NOT_ITE_ELIM)     \
+	FN(NOT_AND)          \
+	FN(CNF_AND_POS)      \
+	FN(CNF_AND_NEG)      \
+	FN(CNF_OR_POS)       \
+	FN(CNF_OR_NEG)       \
+	FN(CNF_IMPLIES_POS)  \
+	FN(CNF_IMPLIES_NEG)  \
+	FN(CNF_EQUIV_POS)    \
+	FN(CNF_EQUIV_NEG)    \
+	FN(CNF_XOR_POS)      \
+	FN(CNF_XOR_NEG)      \
+	FN(CNF_ITE_POS)      \
+	FN(CNF_ITE_NEG)      \
+	FN(ITE_EQ)
+
+enum bcf_bool_rule {
+	BCF_RULE_BOOL_UNSPEC = 0,
+	BCF_BOOL_RULES(BCF_RULE_ENUM_VARIANT)
+	__MAX_BCF_BOOL_RULES,
+};
+
+/* Bitvector proof rules */
+#define BCF_BV_RULES(FN) \
+	FN(BITBLAST)     \
+	FN(POLY_NORM)    \
+	FN(POLY_NORM_EQ)
+
+enum bcf_bv_rule {
+	BCF_RULE_BV_UNSPEC = 0,
+	BCF_BV_RULES(BCF_RULE_ENUM_VARIANT)
+	__MAX_BCF_BV_RULES,
+};
+#undef BCF_RULE_ENUM_VARIANT
+
+#endif /* _UAPI__LINUX_BCF_H__ */
--
2.34.1

[PATCH RFC 02/17] bpf: Add bcf_checker top-level workflow

[Hao Sun]

Introduce the in-kernel BCF proof checker skeleton and public entry point.
The checker validates userspace proofs of refinement conditions.
Proof size hard limit: MAX_BCF_PROOF_SIZE 8M.

kernel/bpf/bcf_checker.c implements:
- Buffer/header validation (check_hdr): enforces BCF_MAGIC, size alignment,
  and overflow-safe size arithmetic for expr/step regions.

- Expression arena load (check_exprs):
  builds a bitmap of validated indices, enforces that each non-VAL argument
  points to an earlier index, stubs type_check() for future semantic checks,
  and records the arena size as the starting point for dynamic ids (id_gen).

- Step load/validation (check_steps): copies steps, verifies per-step size,
  rule class/id bounds via rule_class_max(), that all premises refer to
  strictly earlier steps, records the single ASSUME step (check_assume stub),
  computes last_ref for each step for lifetime mgmt, and requires every
  non-final step to be referenced later.

- Rule application loop (apply_rules): iterates steps in order, dispatches by
  rule class to apply_core_rule/apply_bool_rule/apply_bv_rule (stubs now),

- Memory management: bcf_checker_state owns copied arenas and per-step state;
  dynamically created exprs (facts) are ref-counted, and tracked in an xarray
  indexed by new ids >= expr_size, to be added in the next patch set.

Rule semantics, type checking, and integration with the verifier appear in
later patches; this change only defines the top-level checker structure.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 .clang-format               |   2 +
 include/linux/bcf_checker.h |  18 ++
 kernel/bpf/Makefile         |   2 +-
 kernel/bpf/bcf_checker.c    | 440 ++++++++++++++++++++++++++++++++++++
 4 files changed, 461 insertions(+), 1 deletion(-)
 create mode 100644 include/linux/bcf_checker.h
 create mode 100644 kernel/bpf/bcf_checker.c

diff --git a/.clang-format b/.clang-format
index f371a13b4d19..7f2f85bc4c1f 100644
--- a/.clang-format
+++ b/.clang-format
@@ -747,6 +747,8 @@ ForEachMacros:
   - 'ynl_attr_for_each_nested'
   - 'ynl_attr_for_each_payload'
   - 'zorro_for_each_dev'
+  - 'bcf_for_each_arg'
+  - 'bcf_for_each_pm_step'
 
 IncludeBlocks: Preserve
 IncludeCategories:
diff --git a/include/linux/bcf_checker.h b/include/linux/bcf_checker.h
new file mode 100644
index 000000000000..220552653c80
--- /dev/null
+++ b/include/linux/bcf_checker.h
@@ -0,0 +1,18 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+#ifndef __LINUX_BCF_CHECKER_H__
+#define __LINUX_BCF_CHECKER_H__
+
+#include <uapi/linux/bcf.h>
+#include <linux/stdarg.h>
+#include <linux/bpfptr.h>
+#include <linux/bpf_verifier.h> /* For log level. */
+
+#define MAX_BCF_PROOF_SIZE (8 * 1024 * 1024)
+
+typedef void (*bcf_logger_cb)(void *private, const char *fmt, va_list args);
+
+int bcf_check_proof(struct bcf_expr *goal_exprs, u32 goal, bpfptr_t proof,
+		    u32 proof_size, bcf_logger_cb logger, u32 level,
+		    void *private);
+
+#endif /* __LINUX_BCF_CHECKER_H__ */
diff --git a/kernel/bpf/Makefile b/kernel/bpf/Makefile
index 7fd0badfacb1..5084a0a918e4 100644
--- a/kernel/bpf/Makefile
+++ b/kernel/bpf/Makefile
@@ -6,7 +6,7 @@ cflags-nogcse-$(CONFIG_X86)$(CONFIG_CC_IS_GCC) := -fno-gcse
 endif
 CFLAGS_core.o += -Wno-override-init $(cflags-nogcse-yy)
 
-obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o log.o token.o liveness.o
+obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o log.o token.o liveness.o bcf_checker.o
 obj-$(CONFIG_BPF_SYSCALL) += bpf_iter.o map_iter.o task_iter.o prog_iter.o link_iter.o
 obj-$(CONFIG_BPF_SYSCALL) += hashtab.o arraymap.o percpu_freelist.o bpf_lru_list.o lpm_trie.o map_in_map.o bloom_filter.o
 obj-$(CONFIG_BPF_SYSCALL) += local_storage.o queue_stack_maps.o ringbuf.o
diff --git a/kernel/bpf/bcf_checker.c b/kernel/bpf/bcf_checker.c
new file mode 100644
index 000000000000..33b6e5f04e7f
--- /dev/null
+++ b/kernel/bpf/bcf_checker.c
@@ -0,0 +1,440 @@
+// SPDX-License-Identifier: GPL-2.0-only
+#include <linux/kernel.h>
+#include <linux/overflow.h>
+#include <linux/errno.h>
+#include <linux/export.h>
+#include <linux/cleanup.h>
+#include <linux/slab.h>
+#include <linux/xarray.h>
+#include <linux/refcount.h>
+#include <linux/bitmap.h>
+#include <linux/sched/signal.h>
+#include <linux/sched.h>
+#include <linux/bcf_checker.h>
+
+/* Per proof step state. */
+struct bcf_step_state {
+	/* The conclusion of the current step. */
+	struct bcf_expr *fact;
+	u32 fact_id;
+	/*
+	 * The last step referring to the current step. After `last_ref`, the
+	 * `fact` is no longer used by any other steps and can be freed.
+	 */
+	u32 last_ref;
+};
+
+/*
+ * The expr buffer `exprs` below as well as `steps` rely on the fact that the
+ * size of each arg is the same as the size of the struct bcf_expr, and no
+ * padings in between and after.
+ */
+static_assert(struct_size_t(struct bcf_expr, args, 1) ==
+	      sizeof_field(struct bcf_expr, args[0]) * 2);
+static_assert(struct_size_t(struct bcf_proof_step, args, 1) ==
+	      sizeof_field(struct bcf_proof_step, args[0]) * 2);
+
+/* Size of expr/step in u32 plus the node itself */
+#define EXPR_SZ(expr) ((expr)->vlen + 1)
+#define STEP_SZ(step) ((step)->premise_cnt + (step)->param_cnt + 1)
+
+#define bcf_for_each_arg(arg_id, expr)                                   \
+	for (u32 ___i = 0;                                               \
+	     ___i < (expr)->vlen && (arg_id = (expr)->args[___i], true); \
+	     ___i++)
+
+#define bcf_for_each_pm_step(step_id, step)                      \
+	for (u32 ___i = 0; ___i < (step)->premise_cnt &&         \
+			   (step_id = (step)->args[___i], true); \
+	     ___i++)
+
+struct bcf_checker_state {
+	/*
+	 * Exprs from the proof, referred to as `static expr`. They exist
+	 * during the entire checking phase.
+	 */
+	struct bcf_expr *exprs;
+	/*
+	 * Each expr of `exprs` is followed by their arguments. The `valid_idx`
+	 * bitmap records the valid indices of exprs.
+	 */
+	unsigned long *valid_idx;
+	/* Size of exprs array. */
+	u32 expr_size;
+	/*
+	 * For exprs that are allocated dynamically during proof checking, e.g.,
+	 * conclusions from proof steps, they are refcounted, and each allocated
+	 * expr has an id (increased after `expr_size`) and is stored in xarray.
+	 *
+	 * With this xarray, any routines below can exit early on any error
+	 * without worrying about freeing the exprs allocated; they can be
+	 * freed once when freeing the xarray, see free_checker_state().
+	 */
+	u32 id_gen;
+	struct xarray expr_id_map; /* Id (u32) to `struct bcf_expr_ref` */
+
+	/* Step state tracking */
+	struct bcf_proof_step *steps;
+	struct bcf_step_state *step_state;
+	u32 step_size; /* size of steps array */
+	u32 step_cnt; /* valid number of steps */
+	u32 cur_step;
+	u32 cur_step_idx;
+
+	bcf_logger_cb logger;
+	void *logger_private;
+	u32 level;
+
+	u32 goal;
+	struct bcf_expr *goal_exprs;
+};
+
+static void free_checker_state(struct bcf_checker_state *st)
+{
+	unsigned long id;
+	void *expr;
+
+	kvfree(st->exprs);
+	kvfree(st->valid_idx);
+	xa_for_each(&st->expr_id_map, id, expr) {
+		kfree(expr);
+	}
+	xa_destroy(&st->expr_id_map);
+	kvfree(st->steps);
+	kvfree(st->step_state);
+
+	kfree(st);
+}
+DEFINE_FREE(free_checker, struct bcf_checker_state *,
+	    if (_T) free_checker_state(_T))
+
+__printf(2, 3) static void verbose(struct bcf_checker_state *st,
+				   const char *fmt, ...)
+{
+	va_list args;
+
+	if (!st->logger || !st->level)
+		return;
+	va_start(args, fmt);
+	st->logger(st->logger_private, fmt, args);
+	va_end(args);
+}
+
+/*
+ * Every expr has an id: (1) for static exprs, the idx to `exprs` is its id;
+ * (2) dynamically-allocated ones get one from st->id_gen++.
+ */
+static bool is_static_expr_id(struct bcf_checker_state *st, u32 id)
+{
+	return id < st->expr_size;
+}
+
+/*
+ * Each arg of a bcf_expr must be an id, except for bv_val, which is a
+ * sequence of u32 values.
+ */
+static bool expr_arg_is_id(u8 code)
+{
+	return code != (BCF_BV | BCF_VAL);
+}
+
+static bool is_false(const struct bcf_expr *expr)
+{
+	return expr->code == (BCF_BOOL | BCF_VAL) &&
+	       BCF_BOOL_LITERAL(expr->params) == BCF_FALSE;
+}
+
+/*
+ * Exprs referred to by the proof steps are static exprs from the proof.
+ * Hence, must be valid id in st->exprs.
+ */
+static bool valid_arg_id(struct bcf_checker_state *st, u32 id)
+{
+	return is_static_expr_id(st, id) && test_bit(id, st->valid_idx);
+}
+
+/*
+ * Rather than using:
+ *	if (!correct_condition0 or !correct_condition1)
+ *		return err;
+ * the `ENSURE` macro make this more readable:
+ *	ENSURE(c0 && c1);
+ */
+#define ENSURE(cond)                    \
+	do {                            \
+		if (!(cond))            \
+			return -EINVAL; \
+	} while (0)
+
+static int type_check(struct bcf_checker_state *st, struct bcf_expr *expr)
+{
+	return -EOPNOTSUPP;
+}
+
+static int check_exprs(struct bcf_checker_state *st, bpfptr_t bcf_buf,
+		       u32 expr_size)
+{
+	u32 idx = 0;
+	int err;
+
+	st->exprs =
+		kvmemdup_bpfptr(bcf_buf, expr_size * sizeof(struct bcf_expr));
+	if (IS_ERR(st->exprs)) {
+		err = PTR_ERR(st->exprs);
+		st->exprs = NULL;
+		return err;
+	}
+	st->expr_size = expr_size;
+	st->id_gen = expr_size;
+
+	st->valid_idx = kvzalloc(bitmap_size(expr_size), GFP_KERNEL);
+	if (!st->valid_idx) {
+		kvfree(st->exprs);
+		st->exprs = NULL;
+		return -ENOMEM;
+	}
+
+	while (idx < expr_size) {
+		struct bcf_expr *expr = st->exprs + idx;
+		u32 expr_sz = EXPR_SZ(expr), arg_id;
+
+		ENSURE(idx + expr_sz <= expr_size);
+
+		bcf_for_each_arg(arg_id, expr) {
+			if (!expr_arg_is_id(expr->code))
+				break;
+			/*
+			 * The bitmap enforces that each expr can refer only to
+			 * valid, previous exprs.
+			 */
+			ENSURE(valid_arg_id(st, arg_id));
+		}
+
+		err = type_check(st, expr);
+		if (err)
+			return err;
+
+		set_bit(idx, st->valid_idx);
+		idx += expr_sz;
+	}
+	ENSURE(idx == expr_size);
+
+	return 0;
+}
+
+static int check_assume(struct bcf_checker_state *st,
+			struct bcf_proof_step *step)
+{
+	return -EOPNOTSUPP;
+}
+
+static bool is_assume(u16 rule)
+{
+	return rule == (BCF_RULE_CORE | BCF_RULE_ASSUME);
+}
+
+static u16 rule_class_max(u16 rule)
+{
+	switch (BCF_RULE_CLASS(rule)) {
+	case BCF_RULE_CORE:
+		return __MAX_BCF_CORE_RULES;
+	case BCF_RULE_BOOL:
+		return __MAX_BCF_BOOL_RULES;
+	case BCF_RULE_BV:
+		return __MAX_BCF_BV_RULES;
+	default:
+		return 0;
+	}
+}
+
+static int check_steps(struct bcf_checker_state *st, bpfptr_t bcf_buf,
+		       u32 step_size)
+{
+	u32 pos = 0, cur_step = 0, rule, step_id;
+	struct bcf_proof_step *step;
+	bool goal_found = false;
+	int err;
+
+	st->steps = kvmemdup_bpfptr(bcf_buf,
+				    step_size * sizeof(struct bcf_proof_step));
+	if (IS_ERR(st->steps)) {
+		err = PTR_ERR(st->steps);
+		st->steps = NULL;
+		return err;
+	}
+	st->step_size = step_size;
+
+	/*
+	 * First pass: validate each step and count how many there are.  While
+	 * iterating we also ensure that premises only reference *earlier* steps.
+	 */
+	while (pos < step_size) {
+		step = st->steps + pos;
+		rule = BCF_STEP_RULE(step->rule);
+
+		ENSURE(pos + STEP_SZ(step) <= step_size);
+		ENSURE(rule && rule < rule_class_max(step->rule));
+
+		/* Every step must only refer to previous established steps */
+		bcf_for_each_pm_step(step_id, step)
+			ENSURE(step_id < cur_step);
+
+		/* Must introduce a goal that is consistent to the one required */
+		if (is_assume(step->rule)) {
+			ENSURE(!goal_found); /* only one goal intro step */
+			goal_found = true;
+
+			err = check_assume(st, step);
+			if (err)
+				return err;
+		}
+
+		pos += STEP_SZ(step);
+		cur_step++;
+	}
+
+	/* No trailing garbage and at least two valid steps. */
+	ENSURE(pos == step_size && cur_step >= 2 && goal_found);
+
+	st->step_cnt = cur_step;
+	st->step_state =
+		kvcalloc(cur_step, sizeof(*st->step_state), GFP_KERNEL);
+	if (!st->step_state) {
+		kvfree(st->steps);
+		st->steps = NULL;
+		return -ENOMEM;
+	}
+
+	/* Second pass: fill in last reference index for each step. */
+	for (pos = 0, cur_step = 0; pos < step_size; cur_step++) {
+		step = st->steps + pos;
+		bcf_for_each_pm_step(step_id, step)
+			st->step_state[step_id].last_ref = cur_step;
+
+		pos += STEP_SZ(step);
+	}
+
+	/*
+	 * Every step (except the last one) must be referenced by at
+	 * least one later step.
+	 */
+	for (cur_step = 0; cur_step < st->step_cnt - 1; cur_step++)
+		ENSURE(st->step_state[cur_step].last_ref);
+
+	return 0;
+}
+
+static int apply_core_rule(struct bcf_checker_state *st,
+			   struct bcf_proof_step *step)
+{
+	return -EOPNOTSUPP;
+}
+
+static int apply_bool_rule(struct bcf_checker_state *st,
+			   struct bcf_proof_step *step)
+{
+	return -EOPNOTSUPP;
+}
+
+static int apply_bv_rule(struct bcf_checker_state *st,
+			 struct bcf_proof_step *step)
+{
+	return -EOPNOTSUPP;
+}
+
+static int apply_rules(struct bcf_checker_state *st)
+{
+	struct bcf_expr *fact;
+	int err;
+
+	verbose(st, "checking %u proof steps\n", st->step_cnt);
+
+	while (st->cur_step_idx < st->step_size) {
+		struct bcf_proof_step *step = st->steps + st->cur_step_idx;
+		u16 class = BCF_RULE_CLASS(step->rule);
+
+		if (signal_pending(current))
+			return -EAGAIN;
+		if (need_resched())
+			cond_resched();
+
+		if (class == BCF_RULE_CORE)
+			err = apply_core_rule(st, step);
+		else if (class == BCF_RULE_BOOL)
+			err = apply_bool_rule(st, step);
+		else if (class == BCF_RULE_BV)
+			err = apply_bv_rule(st, step);
+		else {
+			WARN_ONCE(1, "Unknown rule class: %u", class);
+			err = -EFAULT;
+		}
+		if (err)
+			return err;
+
+		st->cur_step_idx += STEP_SZ(step);
+		st->cur_step++;
+	}
+
+	/* The last step must refute the goal by concluding `false` */
+	fact = st->step_state[st->step_cnt - 1].fact;
+	ENSURE(is_false(fact));
+	verbose(st, "proof accepted\n");
+
+	return 0;
+}
+
+static int check_hdr(struct bcf_proof_header *hdr, bpfptr_t proof,
+		     u32 proof_size)
+{
+	u32 expr_size, step_size, sz;
+	bool overflow = false;
+
+	ENSURE(proof_size < MAX_BCF_PROOF_SIZE && proof_size > sizeof(*hdr) &&
+	       (proof_size % sizeof(u32) == 0));
+
+	if (copy_from_bpfptr(hdr, proof, sizeof(*hdr)))
+		return -EFAULT;
+
+	ENSURE(hdr->magic == BCF_MAGIC && hdr->expr_cnt && hdr->step_cnt > 1);
+
+	overflow |= check_mul_overflow(hdr->expr_cnt, sizeof(struct bcf_expr),
+				       &expr_size);
+	overflow |= check_mul_overflow(
+		hdr->step_cnt, sizeof(struct bcf_proof_step), &step_size);
+	overflow |= check_add_overflow(expr_size, step_size, &sz);
+	ENSURE(!overflow && (proof_size - sizeof(*hdr)) == sz);
+
+	return 0;
+}
+
+int bcf_check_proof(struct bcf_expr *goal_exprs, u32 goal, bpfptr_t proof,
+		    u32 proof_size, bcf_logger_cb logger, u32 level,
+		    void *private)
+{
+	struct bcf_checker_state *st __free(free_checker) = NULL;
+	struct bcf_proof_header hdr;
+	int err;
+
+	err = check_hdr(&hdr, proof, proof_size);
+	if (err)
+		return err;
+
+	st = kzalloc(sizeof(*st), GFP_KERNEL_ACCOUNT);
+	if (!st)
+		return -ENOMEM;
+	xa_init(&st->expr_id_map);
+	st->goal_exprs = goal_exprs;
+	st->goal = goal;
+	st->logger = logger;
+	st->logger_private = private;
+	st->level = level;
+
+	bpfptr_add(&proof, sizeof(struct bcf_proof_header));
+	err = check_exprs(st, proof, hdr.expr_cnt);
+
+	bpfptr_add(&proof, hdr.expr_cnt * sizeof(struct bcf_expr));
+	err = err ?: check_steps(st, proof, hdr.step_cnt);
+	err = err ?: apply_rules(st);
+	return err;
+}
+EXPORT_SYMBOL_GPL(bcf_check_proof);
-- 
2.34.1

[PATCH RFC 03/17] bpf: Add UAPI fields for BCF proof interaction

[Hao Sun]

Extend union bpf_attr for BPF_PROG_LOAD to support proof-based verifier
refinement. The new fields let the verifier export the refinement
condition to userspace, preserve its state behind an anon-fd, and later
accept a proof and resume analysis.

- bcf_buf, bcf_buf_size, bcf_buf_true_size: shared buffer used first to
  export expressions+condition to userspace and later to receive a proof.
  true_size refers to the condition size and proof size accordingly.

- bcf_fd: anon-fd that owns the preserved verifier_env. Set by the kernel on
  request; userspace passes it back when submitting a proof.

Tools uapi is also updated.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/uapi/linux/bpf.h       | 21 +++++++++++++++++++++
 kernel/bpf/syscall.c           | 23 ++++++++++++++++++++++-
 tools/include/uapi/linux/bpf.h | 21 +++++++++++++++++++++
 3 files changed, 64 insertions(+), 1 deletion(-)

diff --git a/include/uapi/linux/bpf.h b/include/uapi/linux/bpf.h
index 1d73f165394d..fbe99fbc39ab 100644
--- a/include/uapi/linux/bpf.h
+++ b/include/uapi/linux/bpf.h
@@ -1484,6 +1484,15 @@ enum {
 	BPF_STREAM_STDERR = 2,
 };
 
+/* bcf_flags used in BPF_PROG_LOAD command to indicate if the verifier
+ * requests or the user provides proofs.
+ */
+enum {
+	BCF_F_PROOF_REQUESTED		= (1U << 0),
+	BCF_F_PROOF_PROVIDED		= (1U << 1),
+	BCF_F_PROOF_PATH_UNREACHABLE	= (1U << 2),
+};
+
 union bpf_attr {
 	struct { /* anonymous struct used by BPF_MAP_CREATE command */
 		__u32	map_type;	/* one of enum bpf_map_type */
@@ -1624,6 +1633,18 @@ union bpf_attr {
 		 * verification.
 		 */
 		__s32		keyring_id;
+		/* BCF buffer for both the condition to be proved required by
+		 * the verifier and the proof provided from user space.
+		 */
+		__aligned_u64	bcf_buf;
+		__u32		bcf_buf_size;
+		__u32		bcf_buf_true_size;
+		/* output: BCF fd for loading proof, set by the verifier when
+		 * proof is requested.
+		 */
+		__u32		bcf_fd;
+		/* input/output: proof requested or provided. */
+		__u32		bcf_flags;
 	};
 
 	struct { /* anonymous struct used by BPF_OBJ_* commands */
diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
index 8a129746bd6c..5968b74ed7b2 100644
--- a/kernel/bpf/syscall.c
+++ b/kernel/bpf/syscall.c
@@ -2854,7 +2854,7 @@ static int bpf_prog_verify_signature(struct bpf_prog *prog, union bpf_attr *attr
 }
 
 /* last field in 'union bpf_attr' used by this command */
-#define BPF_PROG_LOAD_LAST_FIELD keyring_id
+#define BPF_PROG_LOAD_LAST_FIELD bcf_flags
 
 static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
 {
@@ -2869,6 +2869,24 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
 	if (CHECK_ATTR(BPF_PROG_LOAD))
 		return -EINVAL;
 
+	if (!!attr->bcf_buf != !!attr->bcf_buf_size ||
+	    (attr->bcf_flags & ~(BCF_F_PROOF_PROVIDED |
+				 BCF_F_PROOF_PATH_UNREACHABLE)))
+		return -EINVAL;
+
+	/* Check proof and resume the last analysis. */
+	if (attr->bcf_flags & BCF_F_PROOF_PROVIDED) {
+		if (attr->bcf_buf_true_size > attr->bcf_buf_size ||
+		    !attr->bcf_buf_size)
+			return -EINVAL;
+		/* The resumed analysis must only uses the old, first attr. */
+		memset(attr, 0, offsetof(union bpf_attr, bcf_buf));
+		return -ENOTSUPP;
+	}
+
+	if (attr->bcf_fd || attr->bcf_buf_true_size || attr->bcf_flags)
+		return -EINVAL;
+
 	if (attr->prog_flags & ~(BPF_F_STRICT_ALIGNMENT |
 				 BPF_F_ANY_ALIGNMENT |
 				 BPF_F_TEST_STATE_FREQ |
@@ -2901,6 +2919,9 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
 	bpf_cap = bpf_token_capable(token, CAP_BPF);
 	err = -EPERM;
 
+	if (attr->bcf_buf && !bpf_cap)
+		goto put_token;
+
 	if (!IS_ENABLED(CONFIG_HAVE_EFFICIENT_UNALIGNED_ACCESS) &&
 	    (attr->prog_flags & BPF_F_ANY_ALIGNMENT) &&
 	    !bpf_cap)
diff --git a/tools/include/uapi/linux/bpf.h b/tools/include/uapi/linux/bpf.h
index 1d73f165394d..fbe99fbc39ab 100644
--- a/tools/include/uapi/linux/bpf.h
+++ b/tools/include/uapi/linux/bpf.h
@@ -1484,6 +1484,15 @@ enum {
 	BPF_STREAM_STDERR = 2,
 };
 
+/* bcf_flags used in BPF_PROG_LOAD command to indicate if the verifier
+ * requests or the user provides proofs.
+ */
+enum {
+	BCF_F_PROOF_REQUESTED		= (1U << 0),
+	BCF_F_PROOF_PROVIDED		= (1U << 1),
+	BCF_F_PROOF_PATH_UNREACHABLE	= (1U << 2),
+};
+
 union bpf_attr {
 	struct { /* anonymous struct used by BPF_MAP_CREATE command */
 		__u32	map_type;	/* one of enum bpf_map_type */
@@ -1624,6 +1633,18 @@ union bpf_attr {
 		 * verification.
 		 */
 		__s32		keyring_id;
+		/* BCF buffer for both the condition to be proved required by
+		 * the verifier and the proof provided from user space.
+		 */
+		__aligned_u64	bcf_buf;
+		__u32		bcf_buf_size;
+		__u32		bcf_buf_true_size;
+		/* output: BCF fd for loading proof, set by the verifier when
+		 * proof is requested.
+		 */
+		__u32		bcf_fd;
+		/* input/output: proof requested or provided. */
+		__u32		bcf_flags;
 	};
 
 	struct { /* anonymous struct used by BPF_OBJ_* commands */
-- 
2.34.1

[PATCH RFC 04/17] bpf: Add top-level workflow of bcf_refine()

[Hao Sun]

Add the top-level refinement hook `bcf_refine()`:

- Add `struct bcf_refine_state` to `struct bpf_verifier_env`: stores the list
  of parent states forming the relevant path suffix (`parents`, `vstate_cnt`),
  and traversal cursors (`cur_vstate`, `cur_jmp_entry`). A boolean `available`
  marks whether BCF can be used in this verification.

- Implement `backtrack_states()`: walking parents with `backtrack_insn()` and
  recorded jump history and find a base state to start the symbolic
  tracking.

- Add a stub `bcf_track()` () and `bcf_refine()` routine that: (a) derives
  default `reg_masks` when not provided by selecting interesting regs,
  (b) backtracks parents, (c) runs `bcf_track()` and a refinement callback,
  and (d) marks the aux flag to request a proof when a condition is produced.

The actual symbolic tracking, condition build and concrete refinements
appear in subsequent patches.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/linux/bpf.h          |   1 +
 include/linux/bpf_verifier.h |  13 +++
 kernel/bpf/verifier.c        | 156 +++++++++++++++++++++++++++++++++++
 3 files changed, 170 insertions(+)

diff --git a/include/linux/bpf.h b/include/linux/bpf.h
index a47d67db3be5..690b0b2b84ba 100644
--- a/include/linux/bpf.h
+++ b/include/linux/bpf.h
@@ -1656,6 +1656,7 @@ struct bpf_prog_aux {
 	bool changes_pkt_data;
 	bool might_sleep;
 	bool kprobe_write_ctx;
+	bool bcf_requested;
 	u64 prog_array_member_cnt; /* counts how many times as member of prog_array */
 	struct mutex ext_mutex; /* mutex for is_extended and prog_array_member_cnt */
 	struct bpf_arena *arena;
diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index c6eb68b6389c..090430168523 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -732,6 +732,18 @@ struct bpf_scc_info {
 
 struct bpf_liveness;
 
+struct bcf_refine_state {
+	/* The state list that decides the path suffix, on which bcf_track()
+	 * collects symbolic information for target registers.
+	 */
+	struct bpf_verifier_state **parents;
+	u32 vstate_cnt;
+	u32 cur_vstate;
+	u32 cur_jmp_entry;
+
+	bool available; /* if bcf_buf is provided. */
+};
+
 /* single container for all structs
  * one verifier_env per bpf_check() call
  */
@@ -838,6 +850,7 @@ struct bpf_verifier_env {
 	struct bpf_scc_info **scc_info;
 	u32 scc_cnt;
 	struct bpf_iarray *succ;
+	struct bcf_refine_state bcf;
 };
 
 static inline struct bpf_func_info_aux *subprog_aux(struct bpf_verifier_env *env, int subprog)
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index e4928846e763..7125f7434e6f 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -608,6 +608,23 @@ static bool is_atomic_load_insn(const struct bpf_insn *insn)
 	       insn->imm == BPF_LOAD_ACQ;
 }
 
+typedef int (*refine_state_fn)(struct bpf_verifier_env *env,
+			       struct bpf_verifier_state *st, void *ctx);
+
+static int bcf_refine(struct bpf_verifier_env *env,
+		      struct bpf_verifier_state *st, u32 reg_masks,
+		      refine_state_fn refine_cb, void *ctx);
+
+static bool bcf_requested(const struct bpf_verifier_env *env)
+{
+	return env->prog->aux->bcf_requested;
+}
+
+static void mark_bcf_requested(struct bpf_verifier_env *env)
+{
+	env->prog->aux->bcf_requested = true;
+}
+
 static int __get_spi(s32 off)
 {
 	return (-off - 1) / BPF_REG_SIZE;
@@ -23378,6 +23395,145 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 	return ret;
 }
 
+static int bcf_track(struct bpf_verifier_env *env,
+		     struct bpf_verifier_state *st,
+		     struct bpf_verifier_state *base)
+{
+	return -EOPNOTSUPP;
+}
+
+/*
+ * Backtracks through parent verifier states to identify the suffix of the path
+ * that is relevant for register refinement in bcf_track(). Using backtrack_insn(),
+ * this routine locates the instructions that define the target registers and any
+ * registers that are transitively related. All states visited during this process
+ * collectively define the path suffix.
+ *
+ * Returns the parent state of the last visited state, which serves as the base
+ * state from which bcf_track() begins its analysis.
+ * The jump history from the collected states determines the suffix to follow.
+ */
+static struct bpf_verifier_state *
+backtrack_states(struct bpf_verifier_env *env, struct bpf_verifier_state *cur,
+		 u32 reg_masks)
+{
+	struct bpf_verifier_state *base = NULL, *st = cur;
+	struct backtrack_state *bt = &env->bt;
+	struct bcf_refine_state *bcf = &env->bcf;
+	int first_idx = cur->first_insn_idx;
+	int last_idx = cur->insn_idx;
+	int subseq_idx = -1;
+	bool skip_first = true;
+	int i, err, log_level = 0;
+	u32 vstate_cnt;
+
+	if (!reg_masks)
+		return ERR_PTR(-EFAULT);
+
+	bt_init(bt, st->curframe);
+	bt->reg_masks[bt->frame] = reg_masks;
+	swap(env->log.level, log_level); /* Disable backtrack_insn() log. */
+
+	for (;;) {
+		u32 history = st->jmp_history_cnt;
+		struct bpf_jmp_history_entry *hist;
+
+		if (last_idx < 0 || !st->parent)
+			break;
+
+		for (i = last_idx;;) {
+			if (skip_first) {
+				err = 0;
+				skip_first = false;
+			} else {
+				hist = get_jmp_hist_entry(st, history, i);
+				err = backtrack_insn(env, i, subseq_idx, hist, bt);
+			}
+			if (err) /* Track the entire path. */
+				goto out;
+			if (bt_empty(bt)) { /* Base state found. */
+				base = st->parent;
+				goto out;
+			}
+			subseq_idx = i;
+			i = get_prev_insn_idx(st, i, &history);
+			if (i == -ENOENT)
+				break;
+			if (i >= env->prog->len)
+				goto out;
+		}
+
+		st = st->parent;
+		subseq_idx = first_idx;
+		last_idx = st->last_insn_idx;
+		first_idx = st->first_insn_idx;
+	}
+
+out:
+	bt_reset(bt);
+	swap(env->log.level, log_level);
+
+	/* Collect parents and follow their jmp history. */
+	vstate_cnt = 1;
+	st = cur->parent;
+	while (st != base) {
+		vstate_cnt++;
+		st = st->parent;
+	}
+	bcf->parents = kmalloc_array(vstate_cnt, sizeof(st), GFP_KERNEL_ACCOUNT);
+	if (!bcf->parents)
+		return ERR_PTR(-ENOMEM);
+	bcf->vstate_cnt = vstate_cnt;
+	st = cur;
+	while (vstate_cnt) {
+		bcf->parents[--vstate_cnt] = st;
+		st = st->parent;
+	}
+	bcf->cur_vstate = 0;
+	bcf->cur_jmp_entry = 0;
+	return base;
+}
+
+static int __used bcf_refine(struct bpf_verifier_env *env,
+			     struct bpf_verifier_state *st, u32 reg_masks,
+			     refine_state_fn refine_cb, void *ctx)
+{
+	struct bpf_reg_state *regs = st->frame[st->curframe]->regs;
+	struct bpf_verifier_state *base;
+	int i, err;
+
+	if (!env->bcf.available || st->speculative)
+		return 0;
+	/* BCF requested multiple times in an error path. */
+	if (bcf_requested(env))
+		return -EFAULT;
+
+	if (!reg_masks) {
+		for (i = 0; i < BPF_REG_FP; i++) {
+			if (regs[i].type == NOT_INIT)
+				continue;
+			if (regs[i].type != SCALAR_VALUE &&
+			    tnum_is_const(regs[i].var_off))
+				continue;
+			reg_masks |= (1 << i);
+		}
+	}
+
+	base = backtrack_states(env, st, reg_masks);
+	if (IS_ERR(base))
+		return PTR_ERR(base);
+
+	err = bcf_track(env, st, base);
+	if (!err && refine_cb)
+		err = refine_cb(env, st, ctx);
+
+	if (!err)
+		mark_bcf_requested(env);
+
+	kfree(env->bcf.parents);
+	return err ?: 1;
+}
+
 /* Lazily verify all global functions based on their BTF, if they are called
  * from main BPF program or any of subprograms transitively.
  * BPF global subprogs called from dead code are not validated.
-- 
2.34.1

[PATCH RFC 05/17] bpf: Add top-level workflow of bcf_track()

[Hao Sun]

Add the top-level `bcf_track()` that symbolically tracks the path suffix
identified by `backtrack_states()` and records per-register expressions and
path conditions.

- Extend `struct bpf_reg_state` with `bcf_expr` index. Extend
  `env->bcf` with tracking state: expression arena (exprs/expr_cnt/expr_size),
  branch condition list (br_conds/br_cond_cnt), and final `path_cond` and
  `refine_cond` index.

- Disable liveness/precision/pruning side effects during tracking to ensure
  single-state, suffix-only analysis (short-circuit early in liveness helpers,
  jump history/push, speculative sanitization, visited-state pruning).

- Implement an env save/restore (`env_backup` + `swap_env_states`) so the
  tracker can reuse verifier execution without polluting global state. 

- After tracking, copy collected `bcf_expr` bindings from the tracked state
  into the original state’s regs. The path condition is built later,

Follow-ups add instruction-specific tracking, path matching and condition
construction into this framework.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/linux/bpf_verifier.h |   9 +++
 kernel/bpf/liveness.c        |  15 ++++
 kernel/bpf/verifier.c        | 135 +++++++++++++++++++++++++++++++++--
 3 files changed, 154 insertions(+), 5 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 090430168523..b430702784e2 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -204,6 +204,7 @@ struct bpf_reg_state {
 	s32 subreg_def;
 	/* if (!precise && SCALAR_VALUE) min/max/tnum don't affect safety */
 	bool precise;
+	int bcf_expr;
 };
 
 enum bpf_stack_slot_type {
@@ -742,6 +743,14 @@ struct bcf_refine_state {
 	u32 cur_jmp_entry;
 
 	bool available; /* if bcf_buf is provided. */
+	bool tracking; /* In bcf_track(). */
+	struct bcf_expr *exprs;
+	u32 expr_size;
+	u32 expr_cnt;
+	u32 *br_conds; /* each branch condition */
+	u32 br_cond_cnt;
+	int path_cond; /* conjunction of br_conds */
+	int refine_cond; /* refinement condition */
 };
 
 /* single container for all structs
diff --git a/kernel/bpf/liveness.c b/kernel/bpf/liveness.c
index bffb495bc933..4e44c3f0404c 100644
--- a/kernel/bpf/liveness.c
+++ b/kernel/bpf/liveness.c
@@ -276,6 +276,8 @@ static struct per_frame_masks *alloc_frame_masks(struct bpf_verifier_env *env,
 
 void bpf_reset_live_stack_callchain(struct bpf_verifier_env *env)
 {
+	if (env->bcf.tracking)
+		return;
 	env->liveness->cur_instance = NULL;
 }
 
@@ -318,6 +320,9 @@ int bpf_mark_stack_read(struct bpf_verifier_env *env, u32 frame, u32 insn_idx, u
 {
 	int err;
 
+	if (env->bcf.tracking)
+		return 0;
+
 	err = ensure_cur_instance(env);
 	err = err ?: mark_stack_read(env, env->liveness->cur_instance, frame, insn_idx, mask);
 	return err;
@@ -339,6 +344,9 @@ int bpf_reset_stack_write_marks(struct bpf_verifier_env *env, u32 insn_idx)
 	struct bpf_liveness *liveness = env->liveness;
 	int err;
 
+	if (env->bcf.tracking)
+		return 0;
+
 	err = ensure_cur_instance(env);
 	if (err)
 		return err;
@@ -349,6 +357,8 @@ int bpf_reset_stack_write_marks(struct bpf_verifier_env *env, u32 insn_idx)
 
 void bpf_mark_stack_write(struct bpf_verifier_env *env, u32 frame, u64 mask)
 {
+	if (env->bcf.tracking)
+		return;
 	env->liveness->write_masks_acc[frame] |= mask;
 }
 
@@ -398,6 +408,8 @@ static int commit_stack_write_marks(struct bpf_verifier_env *env,
  */
 int bpf_commit_stack_write_marks(struct bpf_verifier_env *env)
 {
+	if (env->bcf.tracking)
+		return 0;
 	return commit_stack_write_marks(env, env->liveness->cur_instance);
 }
 
@@ -675,6 +687,9 @@ int bpf_update_live_stack(struct bpf_verifier_env *env)
 	struct func_instance *instance;
 	int err, frame;
 
+	if (env->bcf.tracking)
+		return 0;
+
 	bpf_reset_live_stack_callchain(env);
 	for (frame = env->cur_state->curframe; frame >= 0; --frame) {
 		instance = lookup_instance(env, env->cur_state, frame);
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 7125f7434e6f..725ea503c1c7 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -3924,6 +3924,9 @@ static int push_jmp_history(struct bpf_verifier_env *env, struct bpf_verifier_st
 	struct bpf_jmp_history_entry *p;
 	size_t alloc_size;
 
+	if (env->bcf.tracking)
+		return 0;
+
 	/* combine instruction flags if we already recorded this instruction */
 	if (env->cur_hist_ent) {
 		/* atomic instructions push insn_flags twice, for READ and
@@ -4735,7 +4738,7 @@ static int __mark_chain_precision(struct bpf_verifier_env *env,
 	struct bpf_reg_state *reg;
 	int i, fr, err;
 
-	if (!env->bpf_capable)
+	if (!env->bpf_capable || env->bcf.tracking)
 		return 0;
 
 	changed = changed ?: &tmp;
@@ -8878,6 +8881,9 @@ static struct bpf_verifier_state *find_prev_entry(struct bpf_verifier_env *env,
 	struct bpf_verifier_state *st;
 	struct list_head *pos, *head;
 
+	if (env->bcf.tracking)
+		return NULL;
+
 	/* Explored states are pushed in stack order, most recent states come first */
 	head = explored_state(env, insn_idx);
 	list_for_each(pos, head) {
@@ -14302,7 +14308,8 @@ static bool can_skip_alu_sanitation(const struct bpf_verifier_env *env,
 {
 	return env->bypass_spec_v1 ||
 		BPF_SRC(insn->code) == BPF_K ||
-		cur_aux(env)->nospec;
+		cur_aux(env)->nospec ||
+		env->bcf.tracking;
 }
 
 static int update_alu_sanitation_state(struct bpf_insn_aux_data *aux,
@@ -14350,6 +14357,9 @@ static int sanitize_speculative_path(struct bpf_verifier_env *env,
 	struct bpf_verifier_state *branch;
 	struct bpf_reg_state *regs;
 
+	if (env->bcf.tracking)
+		return 0;
+
 	branch = push_stack(env, next_idx, curr_idx, true);
 	if (!IS_ERR(branch) && insn) {
 		regs = branch->frame[branch->curframe]->regs;
@@ -19415,6 +19425,9 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
 	int n, err, states_cnt = 0;
 	struct list_head *pos, *tmp, *head;
 
+	if (env->bcf.tracking)
+		return 0;
+
 	force_new_state = env->test_state_freq || is_force_checkpoint(env, insn_idx) ||
 			  /* Avoid accumulating infinitely long jmp history */
 			  cur->jmp_history_cnt > 40;
@@ -20076,7 +20089,7 @@ static int do_check(struct bpf_verifier_env *env)
 	struct bpf_insn *insns = env->prog->insnsi;
 	int insn_cnt = env->prog->len;
 	bool do_print_state = false;
-	int prev_insn_idx = -1;
+	int prev_insn_idx = env->prev_insn_idx;
 
 	for (;;) {
 		struct bpf_insn *insn;
@@ -20178,6 +20191,14 @@ static int do_check(struct bpf_verifier_env *env)
 		if (err)
 			return err;
 		err = do_check_insn(env, &do_print_state);
+		/*
+		 * bcf_track() only follows checked insns, errors during it
+		 * indicate a previously refined location; The refinement
+		 * is applied directly (see bcf_refine()), so analyzes the
+		 * insn again with the refined state.
+		 */
+		if (err && env->bcf.tracking)
+			err = do_check_insn(env, &do_print_state);
 		if (err >= 0 || error_recoverable_with_nospec(err)) {
 			marks_err = bpf_commit_stack_write_marks(env);
 			if (marks_err)
@@ -23275,6 +23296,7 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 	struct bpf_reg_state *regs;
 	int ret, i;
 
+	env->prev_insn_idx = -1;
 	env->prev_linfo = NULL;
 	env->pass_cnt++;
 
@@ -23388,6 +23410,10 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 	}
 
 	ret = do_check(env);
+
+	/* Invoked by bcf_track(), just return. */
+	if (env->bcf.tracking)
+		return ret;
 out:
 	if (!ret && pop_log)
 		bpf_vlog_reset(&env->log, 0);
@@ -23395,11 +23421,104 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 	return ret;
 }
 
+struct env_backup {
+	u32 insn_idx;
+	u32 prev_insn_idx;
+	struct bpf_verifier_stack_elem *head;
+	int stack_size;
+	u32 id_gen;
+	struct bpf_verifier_state *cur_state;
+	const struct bpf_line_info *prev_linfo;
+	struct list_head *explored_states;
+	struct list_head free_list;
+	u32 log_level;
+	u32 prev_insn_processed, insn_processed;
+	u32 prev_jmps_processed, jmps_processed;
+};
+
+static void swap_env_states(struct env_backup *env_old,
+			    struct bpf_verifier_env *env)
+{
+	swap(env_old->insn_idx, env->insn_idx);
+	swap(env_old->prev_insn_idx, env->prev_insn_idx);
+	swap(env_old->head, env->head);
+	swap(env_old->stack_size, env->stack_size);
+	swap(env_old->id_gen, env->id_gen);
+	swap(env_old->cur_state, env->cur_state);
+	swap(env_old->prev_linfo, env->prev_linfo);
+	swap(env_old->explored_states, env->explored_states);
+	swap(env_old->free_list, env->free_list);
+	/* Disable log during bcf tracking */
+	swap(env_old->log_level, env->log.level);
+	swap(env_old->prev_insn_processed, env->prev_insn_processed);
+	swap(env_old->insn_processed, env->insn_processed);
+	swap(env_old->prev_jmps_processed, env->prev_jmps_processed);
+	swap(env_old->jmps_processed, env->jmps_processed);
+}
+
 static int bcf_track(struct bpf_verifier_env *env,
 		     struct bpf_verifier_state *st,
 		     struct bpf_verifier_state *base)
 {
-	return -EOPNOTSUPP;
+	struct bpf_reg_state *regs = st->frame[st->curframe]->regs;
+	struct bpf_reg_state *tracked_regs;
+	struct bpf_verifier_state *vstate = NULL;
+	struct env_backup env_old = { 0 };
+	struct bcf_refine_state *bcf = &env->bcf;
+	int err, i;
+
+	bcf->expr_cnt = 0;
+	bcf->path_cond = -1;
+	bcf->refine_cond = -1;
+
+	if (base) {
+		vstate = kzalloc(sizeof(struct bpf_verifier_state),
+				 GFP_KERNEL_ACCOUNT);
+		if (!vstate)
+			return -ENOMEM;
+		err = copy_verifier_state(vstate, base);
+		if (err) {
+			free_verifier_state(vstate, true);
+			return err;
+		}
+		vstate->parent = vstate->equal_state = NULL;
+		vstate->first_insn_idx = base->insn_idx;
+		clear_jmp_history(vstate);
+	}
+
+	/* Continue with the current id. */
+	env_old.id_gen = env->id_gen;
+	swap_env_states(&env_old, env);
+
+	env->bcf.tracking = true;
+	if (vstate) {
+		env->insn_idx = vstate->first_insn_idx;
+		env->prev_insn_idx = vstate->last_insn_idx;
+		env->cur_state = vstate;
+		err = do_check(env);
+	} else {
+		u32 subprog = st->frame[0]->subprogno;
+
+		env->insn_idx = env->subprog_info[subprog].start;
+		err = do_check_common(env, subprog);
+	}
+	env->bcf.tracking = false;
+
+	if (!err && !same_callsites(env->cur_state, st))
+		err = -EFAULT;
+
+	if (!err) {
+		tracked_regs = cur_regs(env);
+		for (i = 0; i < BPF_REG_FP; i++)
+			regs[i].bcf_expr = tracked_regs[i].bcf_expr;
+	}
+
+	free_verifier_state(env->cur_state, true);
+	env->cur_state = NULL;
+	while (!pop_stack(env, NULL, NULL, false))
+		;
+	swap_env_states(&env_old, env);
+	return err;
 }
 
 /*
@@ -23507,6 +23626,12 @@ static int __used bcf_refine(struct bpf_verifier_env *env,
 	/* BCF requested multiple times in an error path. */
 	if (bcf_requested(env))
 		return -EFAULT;
+	/* BCF requested during bcf_track(), known safe just refine. */
+	if (env->bcf.tracking) {
+		if (refine_cb)
+			return refine_cb(env, st, ctx);
+		return 0;
+	}
 
 	if (!reg_masks) {
 		for (i = 0; i < BPF_REG_FP; i++) {
@@ -23527,7 +23652,7 @@ static int __used bcf_refine(struct bpf_verifier_env *env,
 	if (!err && refine_cb)
 		err = refine_cb(env, st, ctx);
 
-	if (!err)
+	if (!err && (env->bcf.refine_cond >= 0 || env->bcf.path_cond >= 0))
 		mark_bcf_requested(env);
 
 	kfree(env->bcf.parents);
-- 
2.34.1

[PATCH RFC 06/17] bpf: Add bcf_match_path() to follow the path suffix

[Hao Sun]

Add `bcf_match_path()` to constrain `bcf_track()` to the recorded path suffix
from parent states. The function consumes the per-state jump history arrays in
order and compares each (prev_idx, idx) pair against the verifier’s current
(prev_insn_idx, insn_idx):

- If the current pair matches the top entry, advance to the next history entry;
  when the last entry is consumed and the last state's last_insn matches, stop
  tracking (PATH_DONE).
- If the pair mismatches at a branch point, abandon the current fork
  (PATH_MISMATCH) so the tracker pops the path.
- Otherwise, continue (PATH_MATCH).

`do_check()` is updated under tracking mode to call `bcf_match_path()` before
processing each instruction and to terminate early on PATH_DONE, ensuring only
suffix instructions are symbolically analyzed.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 66 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 725ea503c1c7..3ecee219605f 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -20082,6 +20082,63 @@ static int do_check_insn(struct bpf_verifier_env *env, bool *do_print_state)
 	return 0;
 }
 
+static struct bpf_jmp_history_entry *
+get_top_jmp_entry(struct bpf_verifier_env *env)
+{
+	struct bcf_refine_state *bcf = &env->bcf;
+	struct bpf_verifier_state *vstate;
+next:
+	if (bcf->cur_vstate >= bcf->vstate_cnt)
+		return NULL;
+	vstate = bcf->parents[bcf->cur_vstate];
+	if (bcf->cur_jmp_entry >= vstate->jmp_history_cnt) {
+		bcf->cur_vstate++;
+		bcf->cur_jmp_entry = 0;
+		goto next;
+	}
+	return &vstate->jmp_history[bcf->cur_jmp_entry];
+}
+
+enum { PATH_MATCH, PATH_MISMATCH, PATH_DONE };
+
+static int bcf_match_path(struct bpf_verifier_env *env)
+{
+	struct bcf_refine_state *bcf = &env->bcf;
+	struct bpf_jmp_history_entry *top = get_top_jmp_entry(env);
+	struct bpf_verifier_state *last_state;
+	int prev_idx;
+
+	last_state = bcf->parents[bcf->vstate_cnt - 1];
+	if (!top)
+		return last_state->last_insn_idx == env->prev_insn_idx ?
+			       PATH_DONE :
+			       PATH_MATCH;
+
+	prev_idx = top->prev_idx;
+	/* entry->prev_idx is u32:20, compiler does not sign extend this */
+	if (prev_idx == 0xfffff)
+		prev_idx = -1;
+
+	if (prev_idx == env->prev_insn_idx) {
+		if (top->idx == env->insn_idx) {
+			bcf->cur_jmp_entry++;
+			/* Check if we have consumed the last entry */
+			top = get_top_jmp_entry(env);
+			if (!top &&
+			    last_state->last_insn_idx == env->prev_insn_idx)
+				return PATH_DONE;
+			return PATH_MATCH;
+		}
+		return PATH_MISMATCH;
+	}
+
+	/* cur_state is branch taken, but the recorded one is not */
+	if (is_jmp_point(env, env->insn_idx))
+		return PATH_MISMATCH;
+
+	return PATH_MATCH;
+}
+
 static int do_check(struct bpf_verifier_env *env)
 {
 	bool pop_log = !(env->log.level & BPF_LOG_LEVEL2);
@@ -20144,6 +20201,15 @@ static int do_check(struct bpf_verifier_env *env)
 				return err;
 		}
 
+		if (env->bcf.tracking) {
+			int path = bcf_match_path(env);
+
+			if (path == PATH_MISMATCH)
+				goto process_bpf_exit;
+			else if (path == PATH_DONE)
+				return 0;
+		}
+
 		if (signal_pending(current))
 			return -EAGAIN;
 
-- 
2.34.1

[PATCH RFC 07/17] bpf: Add bcf_expr management and binding

[Hao Sun]

Add expression arena management for BCF tracking and lazy binding of symbolic
expressions to registers during `bcf_track()`.

- Arena management: `bcf_alloc_expr()` grows `env->bcf.exprs` with
  reallocation in chunks; `bcf_add_expr()` copies a built node; `bcf_build_expr()`
  constructs nodes with varargs.

- Predicates/constraints: `bcf_add_pred()` creates boolean comparisons with an
  immediate RHS; `bcf_add_cond()` appends branch-condition ids into
  `env->bcf.br_conds`.

- Lazy binding: `reg->bcf_expr` starts at -1 and is set on first use via
  `bcf_reg_expr()`. Binding leverages existing range info: if a reg fits in
  u32/s32 ranges, allocate a 32-bit var, add range constraints (u/s min/max),
  then extend to 64-bit with zero/sign extension; otherwise allocate a 64-bit
  var and emit 64-bit bounds. `__check_reg_arg()` binds on first read when
  tracking.

This allows later instruction-specific tracking to refer to previously bound
register expressions and accumulate path constraints.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 280 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 280 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 3ecee219605f..7b6d509c773a 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -4,6 +4,7 @@
  * Copyright (c) 2018 Covalent IO, Inc. http://covalent.io
  */
 #include <uapi/linux/btf.h>
+#include <uapi/linux/bcf.h>
 #include <linux/bpf-cgroup.h>
 #include <linux/kernel.h>
 #include <linux/types.h>
@@ -625,6 +626,275 @@ static void mark_bcf_requested(struct bpf_verifier_env *env)
 	env->prog->aux->bcf_requested = true;
 }
 
+static int bcf_alloc_expr(struct bpf_verifier_env *env, u32 cnt)
+{
+	struct bcf_refine_state *bcf = &env->bcf;
+	int idx = bcf->expr_cnt;
+	struct bcf_expr *exprs;
+	u32 size, alloc_cnt;
+
+	bcf->expr_cnt += cnt;
+	if (bcf->expr_cnt <= bcf->expr_size)
+		return idx;
+
+	alloc_cnt = max_t(u32, 256, cnt);
+	size = size_mul(bcf->expr_size + alloc_cnt, sizeof(struct bcf_expr));
+	exprs = kvrealloc(bcf->exprs, size, GFP_KERNEL_ACCOUNT);
+	if (!exprs) {
+		kvfree(bcf->exprs);
+		bcf->exprs = NULL;
+		return -ENOMEM;
+	}
+	bcf->exprs = exprs;
+	bcf->expr_size += alloc_cnt;
+
+	return idx;
+}
+
+static int bcf_add_expr(struct bpf_verifier_env *env, struct bcf_expr *expr)
+{
+	u32 cnt = (u32)expr->vlen + 1;
+	int idx;
+
+	idx = bcf_alloc_expr(env, cnt);
+	if (idx >= 0)
+		memcpy(env->bcf.exprs + idx, expr,
+		       sizeof(struct bcf_expr) * cnt);
+	return idx;
+}
+
+static int bcf_build_expr(struct bpf_verifier_env *env, u8 code, u16 params,
+			  u32 vlen, ...)
+{
+	DEFINE_RAW_FLEX(struct bcf_expr, expr, args, U8_MAX);
+	va_list args;
+	u32 i;
+
+	if (vlen > U8_MAX)
+		return -EFAULT;
+
+	expr->code = code;
+	expr->vlen = vlen;
+	expr->params = params;
+
+	va_start(args, vlen);
+	for (i = 0; i < vlen; i++) {
+		int arg = va_arg(args, int);
+
+		if (arg < 0)
+			return arg;
+		expr->args[i] = arg;
+	}
+	return bcf_add_expr(env, expr);
+}
+
+static int bcf_add_cond(struct bpf_verifier_env *env, int expr)
+{
+	struct bcf_refine_state *bcf = &env->bcf;
+	u32 cnt = bcf->br_cond_cnt;
+	size_t size;
+	u32 *conds;
+
+	if (expr < 0)
+		return expr;
+	if (cnt >= U8_MAX)
+		return -E2BIG;
+
+	cnt++;
+	size = kmalloc_size_roundup(cnt * sizeof(u32));
+	conds = krealloc(bcf->br_conds, size, GFP_KERNEL_ACCOUNT);
+	if (!conds) {
+		kfree(bcf->br_conds);
+		bcf->br_conds = NULL;
+		return -ENOMEM;
+	}
+	bcf->br_conds = conds;
+	conds[bcf->br_cond_cnt++] = expr;
+	return 0;
+}
+
+static int bcf_val(struct bpf_verifier_env *env, u64 val, bool bit32)
+{
+	DEFINE_RAW_FLEX(struct bcf_expr, expr, args, 2);
+
+	expr->code = BCF_BV | BCF_VAL;
+	expr->vlen = bit32 ? 1 : 2;
+	expr->params = bit32 ? 32 : 64;
+	expr->args[0] = val;
+	if (!bit32)
+		expr->args[1] = val >> 32;
+	return bcf_add_expr(env, expr);
+}
+
+static int bcf_var(struct bpf_verifier_env *env, bool bit32)
+{
+	return bcf_build_expr(env, BCF_BV | BCF_VAR, bit32 ? 32 : 64, 0);
+}
+
+static int bcf_extend(struct bpf_verifier_env *env, u16 ext_sz, u16 bit_sz,
+		      bool sign_ext, int expr)
+{
+	u8 op = sign_ext ? BCF_SIGN_EXTEND : BCF_ZERO_EXTEND;
+
+	return bcf_build_expr(env, BCF_BV | op, (ext_sz << 8) | bit_sz, 1,
+			      expr);
+}
+
+static int bcf_extract(struct bpf_verifier_env *env, u16 sz, int expr)
+{
+	return bcf_build_expr(env, BCF_BV | BCF_EXTRACT, (sz - 1) << 8, 1,
+			      expr);
+}
+
+static int bcf_zext_32_to_64(struct bpf_verifier_env *env,
+			     struct bpf_reg_state *reg)
+{
+	reg->bcf_expr = bcf_extend(env, 32, 64, false, reg->bcf_expr);
+	return reg->bcf_expr;
+}
+
+static int bcf_sext_32_to_64(struct bpf_verifier_env *env,
+			     struct bpf_reg_state *reg)
+{
+	reg->bcf_expr = bcf_extend(env, 32, 64, true, reg->bcf_expr);
+	return reg->bcf_expr;
+}
+
+static bool is_zext_32_to_64(struct bcf_expr *expr)
+{
+	return expr->code == (BCF_BV | BCF_ZERO_EXTEND) &&
+	       expr->params == (((u16)32 << 8) | 64);
+}
+
+static bool is_sext_32_to_64(struct bcf_expr *expr)
+{
+	return expr->code == (BCF_BV | BCF_SIGN_EXTEND) &&
+	       expr->params == (((u16)32 << 8) | 64);
+}
+
+static int bcf_expr32(struct bpf_verifier_env *env, int expr_idx)
+{
+	struct bcf_expr *expr;
+
+	if (expr_idx < 0)
+		return expr_idx;
+
+	expr = env->bcf.exprs + expr_idx;
+	if (is_zext_32_to_64(expr) || is_sext_32_to_64(expr))
+		return expr->args[0];
+
+	if (expr->code == (BCF_BV | BCF_VAL))
+		return bcf_val(env, expr->args[0], true);
+
+	return bcf_extract(env, 32, expr_idx);
+}
+
+static int bcf_add_pred(struct bpf_verifier_env *env, u8 op, int lhs, u64 imm,
+			bool bit32)
+{
+	int rhs;
+
+	if (lhs < 0)
+		return lhs;
+
+	rhs = bcf_val(env, imm, bit32);
+	return bcf_build_expr(env, BCF_BOOL | op, 0, 2, lhs, rhs);
+}
+
+static bool fit_u32(struct bpf_reg_state *reg)
+{
+	return reg->umin_value == reg->u32_min_value &&
+	       reg->umax_value == reg->u32_max_value;
+}
+
+static bool fit_s32(struct bpf_reg_state *reg)
+{
+	return reg->smin_value == reg->s32_min_value &&
+	       reg->smax_value == reg->s32_max_value;
+}
+
+static int __bcf_bound_reg(struct bpf_verifier_env *env, int op, int expr,
+			   u64 imm, bool bit32)
+{
+	return bcf_add_cond(env, bcf_add_pred(env, op, expr, imm, bit32));
+}
+
+static int bcf_bound_reg32(struct bpf_verifier_env *env,
+			   struct bpf_reg_state *reg)
+{
+	u32 umin = reg->u32_min_value, umax = reg->u32_max_value;
+	s32 smin = reg->s32_min_value, smax = reg->s32_max_value;
+	int expr = reg->bcf_expr;
+	int ret = 0;
+
+	if (umin != 0)
+		ret = __bcf_bound_reg(env, BPF_JGE, expr, umin, true);
+	if (ret >= 0 && umax != U32_MAX)
+		ret = __bcf_bound_reg(env, BPF_JLE, expr, umax, true);
+
+	if (ret >= 0 && smin != S32_MIN && smin != umin)
+		ret = __bcf_bound_reg(env, BPF_JSGE, expr, smin, true);
+	if (ret >= 0 && smax != S32_MAX && smax != umax)
+		ret = __bcf_bound_reg(env, BPF_JSLE, expr, smax, true);
+
+	return ret;
+}
+
+static int bcf_bound_reg(struct bpf_verifier_env *env,
+			 struct bpf_reg_state *reg)
+{
+	u64 umin = reg->umin_value, umax = reg->umax_value;
+	s64 smin = reg->smin_value, smax = reg->smax_value;
+	int expr = reg->bcf_expr;
+	int ret = 0;
+
+	if (umin != 0)
+		ret = __bcf_bound_reg(env, BPF_JGE, expr, umin, false);
+	if (ret >= 0 && umax != U64_MAX)
+		ret = __bcf_bound_reg(env, BPF_JLE, expr, umax, false);
+
+	if (ret >= 0 && smin != S64_MIN && smin != umin)
+		ret = __bcf_bound_reg(env, BPF_JSGE, expr, smin, false);
+	if (ret >= 0 && smax != S64_MAX && smax != umax)
+		ret = __bcf_bound_reg(env, BPF_JSLE, expr, smax, false);
+
+	return ret;
+}
+
+static int bcf_reg_expr(struct bpf_verifier_env *env, struct bpf_reg_state *reg,
+			bool subreg)
+{
+	int err;
+
+	if (reg->bcf_expr >= 0)
+		goto out;
+
+	if (tnum_is_const(reg->var_off)) {
+		reg->bcf_expr = bcf_val(env, reg->var_off.value, false);
+	} else if (fit_u32(reg)) {
+		reg->bcf_expr = bcf_var(env, true);
+		err = bcf_bound_reg32(env, reg);
+		if (err < 0)
+			return err;
+		bcf_zext_32_to_64(env, reg);
+	} else if (fit_s32(reg)) {
+		reg->bcf_expr = bcf_var(env, true);
+		err = bcf_bound_reg32(env, reg);
+		if (err < 0)
+			return err;
+		bcf_sext_32_to_64(env, reg);
+	} else {
+		reg->bcf_expr = bcf_var(env, false);
+		err = bcf_bound_reg(env, reg);
+		if (err < 0)
+			return err;
+	}
+out:
+	if (!subreg)
+		return reg->bcf_expr;
+	return bcf_expr32(env, reg->bcf_expr);
+}
+
 static int __get_spi(s32 off)
 {
 	return (-off - 1) / BPF_REG_SIZE;
@@ -2187,6 +2457,8 @@ static void ___mark_reg_known(struct bpf_reg_state *reg, u64 imm)
 	reg->s32_max_value = (s32)imm;
 	reg->u32_min_value = (u32)imm;
 	reg->u32_max_value = (u32)imm;
+
+	reg->bcf_expr = -1;
 }
 
 /* Mark the unknown part of a register (variable offset or scalar value) as
@@ -2807,6 +3079,7 @@ static void __mark_reg_unknown_imprecise(struct bpf_reg_state *reg)
 	reg->var_off = tnum_unknown;
 	reg->frameno = 0;
 	reg->precise = false;
+	reg->bcf_expr = -1;
 	__mark_reg_unbounded(reg);
 }
 
@@ -3790,6 +4063,12 @@ static int __check_reg_arg(struct bpf_verifier_env *env, struct bpf_reg_state *r
 		if (rw64)
 			mark_insn_zext(env, reg);
 
+		/* Bind an expr for non-constants when it's first used. */
+		if (env->bcf.tracking && !tnum_is_const(reg->var_off)) {
+			bcf_reg_expr(env, reg, false);
+			if (reg->bcf_expr < 0)
+				return reg->bcf_expr;
+		}
 		return 0;
 	} else {
 		/* check whether register used as dest operand can be written to */
@@ -25244,6 +25523,7 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	kvfree(env->cfg.insn_postorder);
 	kvfree(env->scc_info);
 	kvfree(env->succ);
+	kvfree(env->bcf.exprs);
 	kvfree(env);
 	return ret;
 }
-- 
2.34.1

[PATCH RFC 08/17] bpf: Track mov and signed extension

[Hao Sun]

Add `bcf_mov()` helpers to model MOV/cast operations in `bcf_track()` and add 
calls into ALU processing paths. The helpers extract the source to the target
width and apply zero/sign extension to the final width as needed.

- For MOV32, build a 32-bit expr for src and zero-extend it.
- For sign-extending MOVs (s8/s16 to W, or s8/s16 to R), extract the sub-width
  and sign-extend to 32 or 64.
- If the destination is known-constant, clear `dst_reg->bcf_expr` (-1) to avoid
  carrying redundant symbolic nodes.

These routines are only active when `env->bcf.tracking` is set. They are called
from `check_alu_op()` in the relevant MOV/SEXT cases.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 69 +++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 66 insertions(+), 3 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 7b6d509c773a..4491d665cc49 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -15959,6 +15959,57 @@ static int adjust_reg_min_max_vals(struct bpf_verifier_env *env,
 	return 0;
 }
 
+static int bcf_mov(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
+		   struct bpf_reg_state *src_reg, u32 sz, bool bit32, bool sext)
+{
+	int src_expr, ext_sz, bitsz = bit32 ? 32 : 64;
+
+	if (!env->bcf.tracking)
+		return 0;
+	if (tnum_is_const(dst_reg->var_off)) {
+		dst_reg->bcf_expr = -1;
+		return 0;
+	}
+
+	src_expr = bcf_reg_expr(env, src_reg, bit32 || sz == 32);
+	if (sz != 32) /* u/s16 u/s8 */
+		src_expr = bcf_extract(env, sz, src_expr);
+
+	if (sext) {
+		ext_sz = bitsz - sz;
+		dst_reg->bcf_expr =
+			bcf_extend(env, ext_sz, bitsz, true, src_expr);
+		if (bit32)
+			bcf_zext_32_to_64(env, dst_reg);
+	} else {
+		ext_sz = 64 - sz;
+		dst_reg->bcf_expr =
+			bcf_extend(env, ext_sz, 64, false, src_expr);
+	}
+	if (dst_reg->bcf_expr < 0)
+		return dst_reg->bcf_expr;
+
+	return 0;
+}
+
+static int bcf_mov32(struct bpf_verifier_env *env, struct bpf_reg_state *dst,
+		     struct bpf_reg_state *src)
+{
+	return bcf_mov(env, dst, src, 32, true, false);
+}
+
+static int bcf_sext32(struct bpf_verifier_env *env, struct bpf_reg_state *dst,
+		      struct bpf_reg_state *src, u32 sz)
+{
+	return bcf_mov(env, dst, src, sz, true, true);
+}
+
+static int bcf_sext64(struct bpf_verifier_env *env, struct bpf_reg_state *dst,
+		      struct bpf_reg_state *src, u32 sz)
+{
+	return bcf_mov(env, dst, src, sz, false, true);
+}
+
 /* check validity of 32-bit and 64-bit arithmetic operations */
 static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 {
@@ -16084,8 +16135,12 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 						if (no_sext)
 							assign_scalar_id_before_mov(env, src_reg);
 						copy_register_state(dst_reg, src_reg);
-						if (!no_sext)
+						if (!no_sext) {
 							dst_reg->id = 0;
+							err = bcf_sext64(env, dst_reg, src_reg, insn->off);
+							if (err)
+								return err;
+						}
 						coerce_reg_to_size_sx(dst_reg, insn->off >> 3);
 						dst_reg->subreg_def = DEF_NOT_SUBREG;
 					} else {
@@ -16110,8 +16165,12 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 						 * range otherwise dst_reg min/max could be incorrectly
 						 * propagated into src_reg by sync_linked_regs()
 						 */
-						if (!is_src_reg_u32)
+						if (!is_src_reg_u32) {
 							dst_reg->id = 0;
+							err = bcf_mov32(env, dst_reg, src_reg);
+							if (err)
+								return err;
+						}
 						dst_reg->subreg_def = env->insn_idx + 1;
 					} else {
 						/* case: W1 = (s8, s16)W2 */
@@ -16120,8 +16179,12 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 						if (no_sext)
 							assign_scalar_id_before_mov(env, src_reg);
 						copy_register_state(dst_reg, src_reg);
-						if (!no_sext)
+						if (!no_sext) {
 							dst_reg->id = 0;
+							err = bcf_sext32(env, dst_reg, src_reg, insn->off);
+							if (err)
+								return err;
+						}
 						dst_reg->subreg_def = env->insn_idx + 1;
 						coerce_subreg_to_size_sx(dst_reg, insn->off >> 3);
 					}
-- 
2.34.1

[PATCH RFC 09/17] bpf: Track alu operations in bcf_track()

[Hao Sun]

Model scalar and pointer ALU operations in the symbolic tracking.

- Scalar ALU: when either operand is non-constant, lazily bind `dst_reg` to a
  symbolic expr and emit the BV op; If both operands are constants, rely on
  the verifier’s result and skip emitting a symbolic node.
  Achieved by hooking `adjust_scalar_min_max_vals()`,

- Pointer ALU: follow verifier logic in `adjust_ptr_min_max_vals()` and record
  only the variable part into `dst_reg->bcf_expr`, carrying constants in
  `reg->off`.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 80 ++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 76 insertions(+), 4 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 4491d665cc49..66682d365e5e 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14865,6 +14865,41 @@ static int sanitize_check_bounds(struct bpf_verifier_env *env,
 	return 0;
 }
 
+static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
+		   struct bpf_reg_state *src_reg, u8 op, bool alu32)
+{
+	DEFINE_RAW_FLEX(struct bcf_expr, alu_expr, args, 2);
+	bool unary = (op == BPF_NEG);
+	int dst, src = 0, bits;
+
+	if (!env->bcf.tracking)
+		return 0;
+	if (tnum_is_const(dst_reg->var_off)) {
+		dst_reg->bcf_expr = -1;
+		return 0;
+	}
+
+	dst = bcf_reg_expr(env, dst_reg, alu32);
+	if (!unary)
+		src = bcf_reg_expr(env, src_reg, alu32);
+	if (dst < 0 || src < 0)
+		return -ENOMEM;
+
+	bits = alu32 ? 32 : 64;
+	alu_expr->code = BCF_BV | op;
+	alu_expr->vlen = unary ? 1 : 2;
+	alu_expr->params = bits;
+	alu_expr->args[0] = dst;
+	alu_expr->args[1] = src;
+	dst_reg->bcf_expr = bcf_add_expr(env, alu_expr);
+	if (alu32)
+		bcf_zext_32_to_64(env, dst_reg);
+	if (dst_reg->bcf_expr < 0)
+		return dst_reg->bcf_expr;
+
+	return 0;
+}
+
 /* Handles arithmetic on a pointer and a scalar: computes new min/max and var_off.
  * Caller should also handle BPF_MOV case separately.
  * If we return -EACCES, caller may want to try again treating pointer as a
@@ -14872,12 +14907,12 @@ static int sanitize_check_bounds(struct bpf_verifier_env *env,
  */
 static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 				   struct bpf_insn *insn,
-				   const struct bpf_reg_state *ptr_reg,
-				   const struct bpf_reg_state *off_reg)
+				   struct bpf_reg_state *ptr_reg,
+				   struct bpf_reg_state *off_reg)
 {
 	struct bpf_verifier_state *vstate = env->cur_state;
 	struct bpf_func_state *state = vstate->frame[vstate->curframe];
-	struct bpf_reg_state *regs = state->regs, *dst_reg;
+	struct bpf_reg_state *regs = state->regs, *dst_reg, *src_reg;
 	bool known = tnum_is_const(off_reg->var_off);
 	s64 smin_val = off_reg->smin_value, smax_val = off_reg->smax_value,
 	    smin_ptr = ptr_reg->smin_value, smax_ptr = ptr_reg->smax_value;
@@ -14889,6 +14924,7 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 	int ret, bounds_ret;
 
 	dst_reg = &regs[dst];
+	src_reg = dst_reg == ptr_reg ? off_reg : ptr_reg;
 
 	if ((known && (smin_val != smax_val || umin_val != umax_val)) ||
 	    smin_val > smax_val || umin_val > umax_val) {
@@ -14989,8 +15025,15 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			dst_reg->var_off = ptr_reg->var_off;
 			dst_reg->off = ptr_reg->off + smin_val;
 			dst_reg->raw = ptr_reg->raw;
+			dst_reg->bcf_expr = ptr_reg->bcf_expr;
 			break;
 		}
+
+		if (env->bcf.tracking) {
+			bcf_reg_expr(env, dst_reg, false);
+			if (dst_reg->bcf_expr < 0)
+				return dst_reg->bcf_expr;
+		}
 		/* A new variable offset is created.  Note that off_reg->off
 		 * == 0, since it's a scalar.
 		 * dst_reg gets the pointer type and since some positive
@@ -15018,6 +15061,10 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			/* something was added to pkt_ptr, set range to zero */
 			memset(&dst_reg->raw, 0, sizeof(dst_reg->raw));
 		}
+
+		ret = bcf_alu(env, dst_reg, src_reg, opcode, false);
+		if (ret)
+			return ret;
 		break;
 	case BPF_SUB:
 		if (dst_reg == off_reg) {
@@ -15046,8 +15093,15 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			dst_reg->id = ptr_reg->id;
 			dst_reg->off = ptr_reg->off - smin_val;
 			dst_reg->raw = ptr_reg->raw;
+			dst_reg->bcf_expr = ptr_reg->bcf_expr;
 			break;
 		}
+
+		if (env->bcf.tracking) {
+			bcf_reg_expr(env, dst_reg, false);
+			if (dst_reg->bcf_expr < 0)
+				return dst_reg->bcf_expr;
+		}
 		/* A new variable offset is created.  If the subtrahend is known
 		 * nonnegative, then any reg->range we had before is still good.
 		 */
@@ -15075,6 +15129,10 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			if (smin_val < 0)
 				memset(&dst_reg->raw, 0, sizeof(dst_reg->raw));
 		}
+
+		ret = bcf_alu(env, dst_reg, src_reg, opcode, false);
+		if (ret)
+			return ret;
 		break;
 	case BPF_AND:
 	case BPF_OR:
@@ -15728,7 +15786,7 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 {
 	u8 opcode = BPF_OP(insn->code);
 	bool alu32 = (BPF_CLASS(insn->code) != BPF_ALU64);
-	int ret;
+	int ret, dst_expr = dst_reg->bcf_expr;
 
 	if (!is_safe_to_compute_dst_reg_range(insn, &src_reg)) {
 		__mark_reg_unknown(env, dst_reg);
@@ -15741,6 +15799,14 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 			return sanitize_err(env, insn, ret, NULL, NULL);
 	}
 
+	/* Constants alu produces constant, skip it; otherwise, bind expr. */
+	if (env->bcf.tracking && (!tnum_is_const(dst_reg->var_off) ||
+				   !tnum_is_const(src_reg.var_off))) {
+		dst_expr = bcf_reg_expr(env, dst_reg, false);
+		if (dst_expr < 0)
+			return dst_expr;
+	}
+
 	/* Calculate sign/unsigned bounds and tnum for alu32 and alu64 bit ops.
 	 * There are two classes of instructions: The first class we track both
 	 * alu32 and alu64 sign/unsigned bounds independently this provides the
@@ -15819,6 +15885,12 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 	if (alu32)
 		zext_32_to_64(dst_reg);
 	reg_bounds_sync(dst_reg);
+
+	dst_reg->bcf_expr = dst_expr;
+	ret = bcf_alu(env, dst_reg, &src_reg, opcode, alu32);
+	if (ret)
+		return ret;
+
 	return 0;
 }
 
-- 
2.34.1

[PATCH RFC 10/17] bpf: Add bcf_alu() 32bits optimization

[Hao Sun]

Lower symbolic ALU nodes to 32-bit when both operands and the resulting dst
fit in 32 bits, to reduce solver/proof complexity.

- Extend `bcf_alu()` with `op_u32`/`op_s32` hints and derive a `zext` decision:
  when ALU32 or both operands/results fit u32, emit a 32-bit op and zero-extend
  to 64; when signed-32 is in effect, sign-extend to 64 after the op.

- Compute `op_u32`/`op_s32` for pointer and scalar ALUs (using fit_u32/fit_s32)
  before emitting the node, then mask them again with the post-ALU dst range so
  the final node width reflects the verifier’s bounds.

This shrinks many BV nodes and helps keep per-node vlen within limits (U8_MAX),
reducing proof size.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 30 +++++++++++++++++++++++++-----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 66682d365e5e..df6d16a1c6f6 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14866,11 +14866,13 @@ static int sanitize_check_bounds(struct bpf_verifier_env *env,
 }
 
 static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
-		   struct bpf_reg_state *src_reg, u8 op, bool alu32)
+		   struct bpf_reg_state *src_reg, u8 op, bool alu32,
+		   bool op_u32, bool op_s32)
 {
 	DEFINE_RAW_FLEX(struct bcf_expr, alu_expr, args, 2);
 	bool unary = (op == BPF_NEG);
 	int dst, src = 0, bits;
+	bool zext = alu32 || op_u32;
 
 	if (!env->bcf.tracking)
 		return 0;
@@ -14879,6 +14881,7 @@ static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
 		return 0;
 	}
 
+	alu32 |= (op_u32 || op_s32);
 	dst = bcf_reg_expr(env, dst_reg, alu32);
 	if (!unary)
 		src = bcf_reg_expr(env, src_reg, alu32);
@@ -14892,8 +14895,11 @@ static int bcf_alu(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
 	alu_expr->args[0] = dst;
 	alu_expr->args[1] = src;
 	dst_reg->bcf_expr = bcf_add_expr(env, alu_expr);
-	if (alu32)
+	if (zext)
 		bcf_zext_32_to_64(env, dst_reg);
+	else if (op_s32)
+		bcf_sext_32_to_64(env, dst_reg);
+
 	if (dst_reg->bcf_expr < 0)
 		return dst_reg->bcf_expr;
 
@@ -14922,6 +14928,7 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 	u8 opcode = BPF_OP(insn->code);
 	u32 dst = insn->dst_reg;
 	int ret, bounds_ret;
+	bool op_u32, op_s32;
 
 	dst_reg = &regs[dst];
 	src_reg = dst_reg == ptr_reg ? off_reg : ptr_reg;
@@ -15034,6 +15041,8 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			if (dst_reg->bcf_expr < 0)
 				return dst_reg->bcf_expr;
 		}
+		op_u32 = fit_u32(dst_reg) && fit_u32(src_reg);
+		op_s32 = fit_s32(dst_reg) && fit_s32(src_reg);
 		/* A new variable offset is created.  Note that off_reg->off
 		 * == 0, since it's a scalar.
 		 * dst_reg gets the pointer type and since some positive
@@ -15062,7 +15071,9 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			memset(&dst_reg->raw, 0, sizeof(dst_reg->raw));
 		}
 
-		ret = bcf_alu(env, dst_reg, src_reg, opcode, false);
+		op_u32 &= fit_u32(dst_reg);
+		op_s32 &= fit_s32(dst_reg);
+		ret = bcf_alu(env, dst_reg, src_reg, opcode, false, op_u32, op_s32);
 		if (ret)
 			return ret;
 		break;
@@ -15102,6 +15113,8 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 			if (dst_reg->bcf_expr < 0)
 				return dst_reg->bcf_expr;
 		}
+		op_u32 = fit_u32(dst_reg) && fit_u32(src_reg);
+		op_s32 = fit_s32(dst_reg) && fit_s32(src_reg);
 		/* A new variable offset is created.  If the subtrahend is known
 		 * nonnegative, then any reg->range we had before is still good.
 		 */
@@ -15130,7 +15143,9 @@ static int adjust_ptr_min_max_vals(struct bpf_verifier_env *env,
 				memset(&dst_reg->raw, 0, sizeof(dst_reg->raw));
 		}
 
-		ret = bcf_alu(env, dst_reg, src_reg, opcode, false);
+		op_u32 &= fit_u32(dst_reg);
+		op_s32 &= fit_s32(dst_reg);
+		ret = bcf_alu(env, dst_reg, src_reg, opcode, false, op_u32, op_s32);
 		if (ret)
 			return ret;
 		break;
@@ -15787,6 +15802,7 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 	u8 opcode = BPF_OP(insn->code);
 	bool alu32 = (BPF_CLASS(insn->code) != BPF_ALU64);
 	int ret, dst_expr = dst_reg->bcf_expr;
+	bool op_u32, op_s32;
 
 	if (!is_safe_to_compute_dst_reg_range(insn, &src_reg)) {
 		__mark_reg_unknown(env, dst_reg);
@@ -15806,6 +15822,8 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 		if (dst_expr < 0)
 			return dst_expr;
 	}
+	op_u32 = fit_u32(dst_reg) && fit_u32(&src_reg);
+	op_s32 = fit_s32(dst_reg) && fit_s32(&src_reg);
 
 	/* Calculate sign/unsigned bounds and tnum for alu32 and alu64 bit ops.
 	 * There are two classes of instructions: The first class we track both
@@ -15887,7 +15905,9 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env,
 	reg_bounds_sync(dst_reg);
 
 	dst_reg->bcf_expr = dst_expr;
-	ret = bcf_alu(env, dst_reg, &src_reg, opcode, alu32);
+	op_u32 &= fit_u32(dst_reg);
+	op_s32 &= fit_s32(dst_reg);
+	ret = bcf_alu(env, dst_reg, &src_reg, opcode, alu32, op_u32, op_s32);
 	if (ret)
 		return ret;
 
-- 
2.34.1

[PATCH RFC 11/17] bpf: Track stack spill/fill in bcf_track()

[Hao Sun]

Track symbolic values across stack spills/fills.

- On spill (`save_register_state()`), if tracking and the source is
  non-constant and the spill is narrower than a full register, derive the
  appropriate-width for the spill slot using `bcf_mov()`.

- On data writes to stack slots (`check_stack_write_*`), invalidate any
  previously spilled pointer symbolic value by setting `spilled_ptr.bcf_expr`
  to -1 when the slot is clobbered.

- On loads that coerce value register sizes (`check_mem_access()`), if the
  destination already has a symbolic expr, cast it to the loaded size via
  `bcf_mov()`.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index df6d16a1c6f6..3f2981db1d40 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -5286,6 +5286,10 @@ static void copy_register_state(struct bpf_reg_state *dst, const struct bpf_reg_
 	*dst = *src;
 }
 
+static int bcf_mov(struct bpf_verifier_env *env, struct bpf_reg_state *dst_reg,
+		   struct bpf_reg_state *src_reg, u32 sz, bool bit32,
+		   bool sext);
+
 static void save_register_state(struct bpf_verifier_env *env,
 				struct bpf_func_state *state,
 				int spi, struct bpf_reg_state *reg,
@@ -5295,6 +5299,11 @@ static void save_register_state(struct bpf_verifier_env *env,
 
 	copy_register_state(&state->stack[spi].spilled_ptr, reg);
 
+	if (env->bcf.tracking && !tnum_is_const(reg->var_off) &&
+	    size != BPF_REG_SIZE)
+		bcf_mov(env, &state->stack[spi].spilled_ptr, reg, size * 8,
+			false, false);
+
 	for (i = BPF_REG_SIZE; i > BPF_REG_SIZE - size; i--)
 		state->stack[spi].slot_type[i - 1] = STACK_SPILL;
 
@@ -5437,6 +5446,7 @@ static int check_stack_write_fixed_off(struct bpf_verifier_env *env,
 
 		/* regular write of data into stack destroys any spilled ptr */
 		state->stack[spi].spilled_ptr.type = NOT_INIT;
+		state->stack[spi].spilled_ptr.bcf_expr = -1;
 		/* Mark slots as STACK_MISC if they belonged to spilled ptr/dynptr/iter. */
 		if (is_stack_slot_special(&state->stack[spi]))
 			for (i = 0; i < BPF_REG_SIZE; i++)
@@ -5566,6 +5576,7 @@ static int check_stack_write_var_off(struct bpf_verifier_env *env,
 
 		/* Erase all other spilled pointers. */
 		state->stack[spi].spilled_ptr.type = NOT_INIT;
+		state->stack[spi].spilled_ptr.bcf_expr = -1;
 
 		/* Update the slot type. */
 		new_type = STACK_MISC;
@@ -8025,6 +8036,11 @@ static int check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regn
 			coerce_reg_to_size(&regs[value_regno], size);
 		else
 			coerce_reg_to_size_sx(&regs[value_regno], size);
+
+		if (env->bcf.tracking && regs[value_regno].bcf_expr >= 0)
+			err = bcf_mov(env, &regs[value_regno],
+				      &regs[value_regno], size * 8, false,
+				      is_ldsx);
 	}
 	return err;
 }
-- 
2.34.1

[PATCH RFC 12/17] bpf: Track path constraint

[Hao Sun]

Record per-branch conditions during `bcf_track()` and build a single
conjunction to represent the path suffix constraint.

- Add `record_path_cond()`: after processing each instruction under tracking,
  examine the previous instruction; if it is a conditional jump over scalars,
  construct a boolean condition that matches the taken/not-taken edge, and then
  append the condition id to `env->bcf.br_conds`.

- When tracking completes, if there are recorded conditions, build
  `env->bcf.path_cond` as either the single condition or a BCF_BOOL|BCF_CONJ
  of all collected conditions.

- In `bcf_refine()`, if both `path_cond` and a refinement-specific
  `refine_cond` exist, combine them via a 2-ary conjunction so userspace proves
  exactly the path-specific condition.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 113 +++++++++++++++++++++++++++++++++++++++---
 1 file changed, 107 insertions(+), 6 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 3f2981db1d40..f1e8e70f9f61 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -20589,6 +20589,70 @@ static int bcf_match_path(struct bpf_verifier_env *env)
 	return PATH_MATCH;
 }
 
+static int record_path_cond(struct bpf_verifier_env *env)
+{
+	int prev_insn_idx = env->prev_insn_idx;
+	struct bpf_reg_state *regs = cur_regs(env);
+	struct bpf_reg_state *dst, *src;
+	int dst_expr, src_expr;
+	struct bpf_insn *insn;
+	u8 class, op, bits;
+	bool jmp32, non_taken;
+	int cond_expr;
+
+	if (prev_insn_idx < 0)
+		return 0;
+
+	insn = &env->prog->insnsi[prev_insn_idx];
+	class = BPF_CLASS(insn->code);
+	op = BPF_OP(insn->code);
+	if (class != BPF_JMP && class != BPF_JMP32)
+		return 0;
+	if (op == BPF_CALL || op == BPF_EXIT || op == BPF_JA || op == BPF_JCOND)
+		return 0;
+	if (insn->off == 0)
+		return 0;
+
+	dst = regs + insn->dst_reg;
+	src = regs + insn->src_reg;
+	if (BPF_SRC(insn->code) == BPF_K) {
+		src = &env->fake_reg[0];
+		memset(src, 0, sizeof(*src));
+		src->type = SCALAR_VALUE;
+		__mark_reg_known(src, insn->imm);
+	}
+	if (dst->type != SCALAR_VALUE || src->type != SCALAR_VALUE)
+		return 0;
+
+	jmp32 = (class == BPF_JMP32);
+	bits = jmp32 ? 32 : 64;
+	dst_expr = bcf_reg_expr(env, dst, jmp32);
+	src_expr = bcf_reg_expr(env, src, jmp32);
+	if (dst_expr < 0 || src_expr < 0)
+		return -ENOMEM;
+
+	non_taken = (prev_insn_idx + 1 == env->insn_idx);
+	if (op == BPF_JSET) {
+		int and_expr, zero_expr;
+
+		and_expr = bcf_build_expr(env, BCF_BV | BPF_AND, bits, 2,
+					  dst_expr, src_expr);
+		zero_expr = bcf_val(env, 0, jmp32);
+		op = BPF_JNE;
+		if (non_taken)
+			op = BPF_JEQ;
+		cond_expr = bcf_build_expr(env, BCF_BOOL | op, 0, 2,
+					   and_expr, zero_expr);
+	} else {
+		if (non_taken)
+			op = rev_opcode(op);
+		cond_expr = bcf_build_expr(env, BCF_BOOL | op, 0, 2, dst_expr,
+					   src_expr);
+	}
+
+	return bcf_add_cond(env, cond_expr);
+}
+
 static int do_check(struct bpf_verifier_env *env)
 {
 	bool pop_log = !(env->log.level & BPF_LOG_LEVEL2);
@@ -20656,8 +20720,9 @@ static int do_check(struct bpf_verifier_env *env)
 
 			if (path == PATH_MISMATCH)
 				goto process_bpf_exit;
-			else if (path == PATH_DONE)
-				return 0;
+			err = record_path_cond(env);
+			if (err || path == PATH_DONE)
+				return err;
 		}
 
 		if (signal_pending(current))
@@ -24023,11 +24088,37 @@ static int bcf_track(struct bpf_verifier_env *env,
 	if (!err && !same_callsites(env->cur_state, st))
 		err = -EFAULT;
 
-	if (!err) {
-		tracked_regs = cur_regs(env);
-		for (i = 0; i < BPF_REG_FP; i++)
-			regs[i].bcf_expr = tracked_regs[i].bcf_expr;
+	if (err)
+		goto out;
+
+	tracked_regs = cur_regs(env);
+	for (i = 0; i < BPF_REG_FP; i++)
+		regs[i].bcf_expr = tracked_regs[i].bcf_expr;
+
+	/* Build the path constraint. */
+	if (bcf->br_cond_cnt == 1) {
+		bcf->path_cond = *bcf->br_conds;
+	} else if (bcf->br_cond_cnt > 1) {
+		struct bcf_expr *cond_expr;
+		int cond;
+
+		cond = bcf_alloc_expr(env, bcf->br_cond_cnt + 1);
+		if (cond < 0) {
+			err = cond;
+			goto out;
+		}
+		cond_expr = bcf->exprs + cond;
+		cond_expr->code = BCF_BOOL | BCF_CONJ;
+		cond_expr->params = 0;
+		cond_expr->vlen = bcf->br_cond_cnt;
+		memcpy(cond_expr->args, bcf->br_conds,
+		       sizeof(u32) * bcf->br_cond_cnt);
+		bcf->path_cond = cond;
 	}
+out:
+	kfree(bcf->br_conds);
+	bcf->br_conds = NULL;
+	bcf->br_cond_cnt = 0;
 
 	free_verifier_state(env->cur_state, true);
 	env->cur_state = NULL;
@@ -24134,6 +24225,7 @@ static int __used bcf_refine(struct bpf_verifier_env *env,
 			     refine_state_fn refine_cb, void *ctx)
 {
 	struct bpf_reg_state *regs = st->frame[st->curframe]->regs;
+	struct bcf_refine_state *bcf = &env->bcf;
 	struct bpf_verifier_state *base;
 	int i, err;
 
@@ -24168,6 +24260,15 @@ static int __used bcf_refine(struct bpf_verifier_env *env,
 	if (!err && refine_cb)
 		err = refine_cb(env, st, ctx);
 
+	/* The final condition is the conj of path_cond and refine_cond. */
+	if (!err && bcf->refine_cond >= 0 && bcf->path_cond >= 0) {
+		bcf->refine_cond = bcf_build_expr(env, BCF_BOOL | BCF_CONJ, 0,
+						  2, bcf->path_cond,
+						  bcf->refine_cond);
+		if (bcf->refine_cond < 0)
+			err = bcf->refine_cond;
+	}
+
 	if (!err && (env->bcf.refine_cond >= 0 || env->bcf.path_cond >= 0))
 		mark_bcf_requested(env);
 
-- 
2.34.1

[PATCH RFC 13/17] bpf: Skip state pruning for the parent states

[Hao Sun]

Different incoming paths to the same instruction may yield different path
conditions; pruning by containment would drop paths with different constraints.

- Add `children_unsafe` flag to `struct bpf_verifier_state`.
- In `is_state_visited()`, if a visited candidate has `children_unsafe`, treat
  it as a miss.
- Propagate `children_unsafe` to the next state on split and clear it in the
  current state when pushing a new parent.
- After a refinement request, clear all `bcf_expr` in registers and mark all
  collected parents (except the base) as `children_unsafe` to avoid pruning
  alternative suffixes that may build different path conditions.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/linux/bpf_verifier.h |  1 +
 kernel/bpf/verifier.c        | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index b430702784e2..9b91353a86d7 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -422,6 +422,7 @@ struct bpf_verifier_state {
 	bool speculative;
 	bool in_sleepable;
 	bool cleaned;
+	bool children_unsafe;
 
 	/* first and last insn idx of this verifier state */
 	u32 first_insn_idx;
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index f1e8e70f9f61..ec0e736f39c5 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -19904,6 +19904,8 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
 		states_cnt++;
 		if (sl->state.insn_idx != insn_idx)
 			continue;
+		if (sl->state.children_unsafe)
+			goto miss;
 
 		if (sl->state.branches) {
 			struct bpf_func_state *frame = sl->state.frame[sl->state.curframe];
@@ -20216,6 +20218,8 @@ static int is_state_visited(struct bpf_verifier_env *env, int insn_idx)
 		return err;
 	}
 
+	new->children_unsafe = cur->children_unsafe;
+	cur->children_unsafe = false;
 	cur->parent = new;
 	cur->first_insn_idx = insn_idx;
 	cur->dfs_depth = new->dfs_depth + 1;
@@ -24272,6 +24276,20 @@ static int __used bcf_refine(struct bpf_verifier_env *env,
 	if (!err && (env->bcf.refine_cond >= 0 || env->bcf.path_cond >= 0))
 		mark_bcf_requested(env);
 
+	for (i = 0; i < MAX_BPF_REG; i++)
+		regs[i].bcf_expr = -1;
+
+	/*
+	 * Mark the parents as children_unsafe, i.e., they are not safe for
+	 * state pruning anymore. Say s0 is contained in s1 (marked), then
+	 * exploring s0 will reach the same error state that triggers the
+	 * refinement. However, since the path they reach the pruning point
+	 * can be different, the path condition collected for s0 can be
+	 * different from s1's. Hence, pruning is not safe.
+	 */
+	for (i = 0; i < bcf->vstate_cnt - 1; i++)
+		bcf->parents[i]->children_unsafe = true;
+
 	kfree(env->bcf.parents);
 	return err ?: 1;
 }
-- 
2.34.1

[PATCH RFC 14/17] bpf: Add mem access bound refinement

[Hao Sun]

Implement on-demand refinement for memory access bound checks and add 
fallback to path-unreachable when refinement is not applicable.

When common bound checks (stack/map/packet) fail (min/max outside bounds) or
certain helper memory checks fail with -EACCES, call into `bcf_refine()` to
prove either: (a) tighter bounds on pointer offset or size make the access
safe, or (b) the current path is unreachable. For -EACCES on other sites, try
path-unreachable directly (`bcf_prove_unreachable()`). If the same error point
is re-encountered under tracking, refinement is applied directly without a new
proof since they are known safe.

- __bcf_refine_access_bound():
  * const ptr + var size: prove `off + size_expr <= high` and refine size
    upper bound accordingly; the condition emitted is JGT, expects the
    solver to prove it unsat.
  * var ptr + const size: prove `fix_off + off_expr + sz <= high` and if needed,
    `off + off_expr >= low`; refine pointer smin/smax accordingly.
  * var ptr + var size: emit two constraints (sum <= high and ptr_off >= low),
    and if proved, treat the access as safe for range [smin, high) without
    changing either reg as the source of imprecision is unknown.
    Mark current state’s children as unsafe for pruning.

  * Split `check_mem_access()` into `do_check_mem_access()` and a wrapper that
    triggers path-unreachable on -EACCES when no request was made yet.
  * Wrap `check_helper_mem_access()` similarly and integrate `check_mem_size_reg()`
    with `access_checked` fast path to re-check a proven safe range by
    temporarily constraining the pointer reg.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/linux/bpf_verifier.h |   6 +
 kernel/bpf/verifier.c        | 262 +++++++++++++++++++++++++++++++++--
 2 files changed, 255 insertions(+), 13 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 9b91353a86d7..05e8e3feea30 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -752,6 +752,12 @@ struct bcf_refine_state {
 	u32 br_cond_cnt;
 	int path_cond; /* conjunction of br_conds */
 	int refine_cond; /* refinement condition */
+
+	/* Refinement specific */
+	u32 size_regno;
+	int checked_off;
+	int checked_sz;
+	bool access_checked;
 };
 
 /* single container for all structs
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index ec0e736f39c5..22a068bfd0f2 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -621,6 +621,16 @@ static bool bcf_requested(const struct bpf_verifier_env *env)
 	return env->prog->aux->bcf_requested;
 }
 
+static void bcf_prove_unreachable(struct bpf_verifier_env *env)
+{
+	int err;
+
+	err = bcf_refine(env, env->cur_state, 0, NULL, NULL);
+	if (!err)
+		verbose(env,
+			"bcf requested, try to prove the path unreachable\n");
+}
+
 static void mark_bcf_requested(struct bpf_verifier_env *env)
 {
 	env->prog->aux->bcf_requested = true;
@@ -4088,8 +4098,12 @@ static int check_reg_arg(struct bpf_verifier_env *env, u32 regno,
 {
 	struct bpf_verifier_state *vstate = env->cur_state;
 	struct bpf_func_state *state = vstate->frame[vstate->curframe];
+	int err;
 
-	return __check_reg_arg(env, state->regs, regno, t);
+	err = __check_reg_arg(env, state->regs, regno, t);
+	if (err == -EACCES && !bcf_requested(env))
+		bcf_prove_unreachable(env);
+	return err;
 }
 
 static int insn_stack_access_flags(int frameno, int spi)
@@ -5256,6 +5270,163 @@ static bool __is_pointer_value(bool allow_ptr_leaks,
 	return reg->type != SCALAR_VALUE;
 }
 
+struct bcf_mem_access_refine_ctx {
+	struct bpf_reg_state *ptr_reg;
+	struct bpf_reg_state *size_reg;
+	s32 off;
+	s32 lower_bound;
+	s32 higher_bound;
+};
+
+static int __bcf_refine_access_bound(struct bpf_verifier_env *env,
+				     struct bpf_verifier_state *st,
+				     void *access)
+{
+	struct bcf_mem_access_refine_ctx *ctx = access;
+	struct bpf_reg_state *size_reg = ctx->size_reg, *ptr_reg = ctx->ptr_reg;
+	u32 mem_sz = ctx->higher_bound - ctx->lower_bound;
+	int size_expr, off_expr, low_expr, high_expr;
+	struct bcf_refine_state *bcf = &env->bcf;
+	s32 off = ctx->off;
+	s64 min_off, max_off;
+	bool bit32 = false;
+
+	off_expr = ptr_reg->bcf_expr;
+	size_expr = size_reg->bcf_expr;
+	if (fit_s32(ptr_reg) && fit_s32(size_reg)) {
+		off_expr = bcf_expr32(env, off_expr);
+		size_expr = bcf_expr32(env, size_expr);
+		bit32 = true;
+	}
+
+	min_off = ptr_reg->smin_value + off;
+	max_off = ptr_reg->smax_value + off;
+
+	if (tnum_is_const(ptr_reg->var_off)) { /* Refine the size range */
+		off += ptr_reg->var_off.value;
+
+		/* Prove `off + size > higher_bound` unsatisfiable */
+		bcf->refine_cond = bcf_add_pred(env, BPF_JGT, size_expr,
+						ctx->higher_bound - off, bit32);
+
+		/* size->umax + off <= higher holds after proof */
+		size_reg->umax_value = ctx->higher_bound - off;
+		size_reg->umin_value =
+			min_t(u64, size_reg->umax_value, size_reg->umin_value);
+		reg_bounds_sync(size_reg);
+
+	} else if (tnum_is_const(size_reg->var_off)) { /* Refine the ptr off */
+		u32 sz = size_reg->var_off.value;
+
+		/* Prove `off + off_expr + sz > higher_bound` unsatisfiable */
+		high_expr = bcf_add_pred(env, BPF_JSGT, off_expr,
+					 ctx->higher_bound - sz - off, bit32);
+		/*
+		 * If the verifier already knows the lower bound is safe, then
+		 * don't emit this in the formula.
+		 */
+		bcf->refine_cond = high_expr;
+		if (min_off < ctx->lower_bound) {
+			low_expr = bcf_add_pred(env, BPF_JSLT, off_expr,
+						ctx->lower_bound - off, bit32);
+			bcf->refine_cond =
+				bcf_build_expr(env, BCF_BOOL | BCF_DISJ, 0, 2,
+					       low_expr, high_expr);
+		}
+
+		if (min_off < ctx->lower_bound)
+			ptr_reg->smin_value = ctx->lower_bound - off;
+		if (max_off + sz > ctx->higher_bound)
+			ptr_reg->smax_value = ctx->higher_bound - off - sz;
+		reg_bounds_sync(ptr_reg);
+	} else { /* Prove var off with var size is safe */
+		u32 bitsz = bit32 ? 32 : 64;
+
+		high_expr = bcf_build_expr(env, BCF_BV | BPF_ADD, bitsz, 2,
+					   off_expr, size_expr);
+		high_expr = bcf_add_pred(env, BPF_JSGT, high_expr,
+					 ctx->higher_bound - off, bit32);
+		bcf->refine_cond = high_expr;
+		if (min_off < ctx->lower_bound) {
+			low_expr = bcf_add_pred(env, BPF_JSLT, off_expr,
+						ctx->lower_bound - off, bit32);
+			bcf->refine_cond =
+				bcf_build_expr(env, BCF_BOOL | BCF_DISJ, 0, 2,
+					       low_expr, high_expr);
+		}
+
+		if (min_off < ctx->lower_bound)
+			ptr_reg->smin_value = ctx->lower_bound - off;
+		if (max_off > ctx->higher_bound)
+			ptr_reg->smax_value = ctx->higher_bound - off;
+		if (size_reg->umax_value > mem_sz)
+			size_reg->umax_value = mem_sz;
+		reg_bounds_sync(ptr_reg);
+		reg_bounds_sync(size_reg);
+
+		/*
+		 * off+off_expr+sz_expr <= high && off+off_expr>=low proved,
+		 * but it's not clear which regs are the source of imprecision;
+		 * hence don't refine, but remember the access is safe and
+		 * treat this access as [smin, higher) range access.
+		 */
+		min_off = ptr_reg->smin_value + off;
+		bcf->checked_off = ptr_reg->smin_value;
+		bcf->checked_sz = ctx->higher_bound - min_off;
+		bcf->access_checked = true;
+		st->children_unsafe = true;
+	}
+
+	return bcf->refine_cond < 0 ? bcf->refine_cond : 0;
+}
+
+static void bcf_refine_access_bound(struct bpf_verifier_env *env, int regno,
+				    s32 off, s32 low, s32 high, u32 access_size)
+{
+	struct bcf_mem_access_refine_ctx ctx = {
+		.off = off,
+		.lower_bound = low,
+		.higher_bound = high,
+	};
+	struct bpf_reg_state *regs = cur_regs(env), tmp_reg;
+	struct bpf_reg_state *ptr_reg, *size_reg;
+	struct bcf_refine_state *bcf = &env->bcf;
+	u32 reg_masks = 0, mem_sz = high - low;
+	bool ptr_const, size_const;
+	s64 ptr_off;
+	int err;
+
+	ptr_reg = regs + regno;
+	ptr_const = tnum_is_const(ptr_reg->var_off);
+	if (!ptr_const)
+		reg_masks |= (1 << regno);
+
+	__mark_reg_known(&tmp_reg, access_size);
+	tmp_reg.type = SCALAR_VALUE;
+	size_reg = &tmp_reg;
+	if (bcf->size_regno > 0) {
+		size_reg = regs + bcf->size_regno;
+		if (!tnum_is_const(size_reg->var_off))
+			reg_masks |= (1 << bcf->size_regno);
+	}
+	size_const = tnum_is_const(size_reg->var_off);
+	ctx.size_reg = size_reg;
+	ctx.ptr_reg = ptr_reg;
+
+	/* Prove unreachable. */
+	ptr_off = ptr_reg->smin_value + off;
+	if (!reg_masks || !mem_sz ||
+	    (ptr_const && (ptr_off < low || ptr_off >= high)) ||
+	    (size_const && size_reg->var_off.value > mem_sz))
+		return bcf_prove_unreachable(env);
+
+	err = bcf_refine(env, env->cur_state, reg_masks,
+			 __bcf_refine_access_bound, &ctx);
+	if (!err)
+		verbose(env, "bcf requested, try to refine R%d access\n",
+			regno);
+}
+
 static void assign_scalar_id_before_mov(struct bpf_verifier_env *env,
 					struct bpf_reg_state *src_reg)
 {
@@ -6016,6 +6187,7 @@ static int check_mem_region_access(struct bpf_verifier_env *env, u32 regno,
 	if (err) {
 		verbose(env, "R%d min value is outside of the allowed memory range\n",
 			regno);
+		bcf_refine_access_bound(env, regno, off, 0, mem_size, size);
 		return err;
 	}
 
@@ -6033,6 +6205,7 @@ static int check_mem_region_access(struct bpf_verifier_env *env, u32 regno,
 	if (err) {
 		verbose(env, "R%d max value is outside of the allowed memory range\n",
 			regno);
+		bcf_refine_access_bound(env, regno, off, 0, mem_size, size);
 		return err;
 	}
 
@@ -7680,6 +7853,15 @@ static int check_ptr_to_map_access(struct bpf_verifier_env *env,
 	return 0;
 }
 
+static int stack_min_off(struct bpf_verifier_env *env, struct bpf_func_state *state,
+			 enum bpf_access_type t)
+{
+	if (t == BPF_WRITE || env->allow_uninit_stack)
+		return -MAX_BPF_STACK;
+	else
+		return -state->allocated_stack;
+}
+
 /* Check that the stack access at the given offset is within bounds. The
  * maximum valid offset is -1.
  *
@@ -7693,11 +7875,7 @@ static int check_stack_slot_within_bounds(struct bpf_verifier_env *env,
 {
 	int min_valid_off;
 
-	if (t == BPF_WRITE || env->allow_uninit_stack)
-		min_valid_off = -MAX_BPF_STACK;
-	else
-		min_valid_off = -state->allocated_stack;
-
+	min_valid_off = stack_min_off(env, state, t);
 	if (off < min_valid_off || off > -1)
 		return -EACCES;
 	return 0;
@@ -7759,6 +7937,11 @@ static int check_stack_access_within_bounds(
 			verbose(env, "invalid variable-offset%s stack R%d var_off=%s off=%d size=%d\n",
 				err_extra, regno, tn_buf, off, access_size);
 		}
+
+		if (err != -EFAULT)
+			bcf_refine_access_bound(env, regno, off,
+						stack_min_off(env, state, type),
+						0, access_size);
 		return err;
 	}
 
@@ -7785,7 +7968,7 @@ static bool get_func_retval_range(struct bpf_prog *prog,
  * if t==write && value_regno==-1, some unknown value is stored into memory
  * if t==read && value_regno==-1, don't care what we read from memory
  */
-static int check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regno,
+static int do_check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regno,
 			    int off, int bpf_size, enum bpf_access_type t,
 			    int value_regno, bool strict_alignment_once, bool is_ldsx)
 {
@@ -8045,6 +8228,20 @@ static int check_mem_access(struct bpf_verifier_env *env, int insn_idx, u32 regn
 	return err;
 }
 
+static int check_mem_access(struct bpf_verifier_env *env, int insn_idx,
+			    u32 regno, int off, int bpf_size,
+			    enum bpf_access_type t, int value_regno,
+			    bool strict_alignment_once, bool is_ldsx)
+{
+	int err;
+
+	err = do_check_mem_access(env, insn_idx, regno, off, bpf_size, t,
+			       value_regno, strict_alignment_once, is_ldsx);
+	if (err == -EACCES && !bcf_requested(env))
+		bcf_prove_unreachable(env);
+	return err;
+}
+
 static int save_aux_ptr_type(struct bpf_verifier_env *env, enum bpf_reg_type type,
 			     bool allow_trust_mismatch);
 
@@ -8427,7 +8624,7 @@ static int check_stack_range_initialized(
 	return 0;
 }
 
-static int check_helper_mem_access(struct bpf_verifier_env *env, int regno,
+static int __check_helper_mem_access(struct bpf_verifier_env *env, int regno,
 				   int access_size, enum bpf_access_type access_type,
 				   bool zero_size_allowed,
 				   struct bpf_call_arg_meta *meta)
@@ -8518,6 +8715,21 @@ static int check_helper_mem_access(struct bpf_verifier_env *env, int regno,
 	}
 }
 
+static int check_helper_mem_access(struct bpf_verifier_env *env, int regno,
+				   int access_size,
+				   enum bpf_access_type access_type,
+				   bool zero_size_allowed,
+				   struct bpf_call_arg_meta *meta)
+{
+	int err;
+
+	err = __check_helper_mem_access(env, regno, access_size, access_type,
+					zero_size_allowed, meta);
+	if (err == -EACCES && !bcf_requested(env))
+		bcf_prove_unreachable(env);
+	return err;
+}
+
 /* verify arguments to helpers or kfuncs consisting of a pointer and an access
  * size.
  *
@@ -8530,6 +8742,7 @@ static int check_mem_size_reg(struct bpf_verifier_env *env,
 			      bool zero_size_allowed,
 			      struct bpf_call_arg_meta *meta)
 {
+	struct bcf_refine_state *bcf = &env->bcf;
 	int err;
 
 	/* This is used to refine r0 return value bounds for helpers
@@ -8553,22 +8766,40 @@ static int check_mem_size_reg(struct bpf_verifier_env *env,
 	if (reg->smin_value < 0) {
 		verbose(env, "R%d min value is negative, either use unsigned or 'var &= const'\n",
 			regno);
+		bcf_prove_unreachable(env);
 		return -EACCES;
 	}
 
 	if (reg->umin_value == 0 && !zero_size_allowed) {
 		verbose(env, "R%d invalid zero-sized read: u64=[%lld,%lld]\n",
 			regno, reg->umin_value, reg->umax_value);
+		bcf_prove_unreachable(env);
 		return -EACCES;
 	}
 
 	if (reg->umax_value >= BPF_MAX_VAR_SIZ) {
 		verbose(env, "R%d unbounded memory access, use 'var &= const' or 'if (var < const)'\n",
 			regno);
+		bcf_prove_unreachable(env);
 		return -EACCES;
 	}
-	err = check_helper_mem_access(env, regno - 1, reg->umax_value,
+
+	if (bcf->access_checked) {
+		struct bpf_reg_state *ptr_reg = &cur_regs(env)[regno - 1];
+		struct bpf_reg_state tmp = *ptr_reg;
+
+		___mark_reg_known(ptr_reg, bcf->checked_off);
+		err = check_helper_mem_access(env, regno - 1, bcf->checked_sz,
+					      access_type, zero_size_allowed, meta);
+		*ptr_reg = tmp;
+		bcf->access_checked = false;
+	} else {
+		bcf->size_regno = regno;
+		err = check_helper_mem_access(env, regno - 1, reg->umax_value,
 				      access_type, zero_size_allowed, meta);
+		bcf->size_regno = 0;
+	}
+
 	if (!err)
 		err = mark_chain_precision(env, regno);
 	return err;
@@ -16367,8 +16598,11 @@ static int check_alu_op(struct bpf_verifier_env *env, struct bpf_insn *insn)
 		/* check dest operand */
 		err = check_reg_arg(env, insn->dst_reg, DST_OP_NO_MARK);
 		err = err ?: adjust_reg_min_max_vals(env, insn);
-		if (err)
+		if (err) {
+			if (!bcf_requested(env))
+				bcf_prove_unreachable(env);
 			return err;
+		}
 	}
 
 	return reg_bounds_sanity_check(env, &regs[insn->dst_reg], "alu");
@@ -20474,6 +20708,8 @@ static int do_check_insn(struct bpf_verifier_env *env, bool *do_print_state)
 			} else {
 				err = check_helper_call(env, insn, &env->insn_idx);
 			}
+			if (err == -EACCES && !bcf_requested(env))
+				bcf_prove_unreachable(env);
 			if (err)
 				return err;
 
@@ -24224,9 +24460,9 @@ backtrack_states(struct bpf_verifier_env *env, struct bpf_verifier_state *cur,
 	return base;
 }
 
-static int __used bcf_refine(struct bpf_verifier_env *env,
-			     struct bpf_verifier_state *st, u32 reg_masks,
-			     refine_state_fn refine_cb, void *ctx)
+static int bcf_refine(struct bpf_verifier_env *env,
+		      struct bpf_verifier_state *st, u32 reg_masks,
+		      refine_state_fn refine_cb, void *ctx)
 {
 	struct bpf_reg_state *regs = st->frame[st->curframe]->regs;
 	struct bcf_refine_state *bcf = &env->bcf;
-- 
2.34.1

[PATCH RFC 15/17] bpf: Preserve verifier_env and request BCF

[Hao Sun]

Preserve the verifier environment when a refinement request is issued and
export the expression arena and condition to userspace, so that the analysis
can resume later with a proof.

- Track the currently analyzed subprog (`env->subprog`) so resume can pick up
  where the request occurred. 
- In `do_check_common()`, if a request is pending, return early without
  freeing states (bcf/tracking-aware). In `bpf_prog_load()`, if the request was
  issued, return the verifier error immediately to userspace.
- Add anon-fd : create an anon inode (`bcf_fops`) that owns the `verifier_env`.
  On fd release, free verifier state, release maps/btfs/prog.
- Implement `do_request_bcf()`: copy conditions into `bcf_buf`; set
  `bcf_flags = BCF_F_PROOF_REQUESTED`; allocate and return
  `bcf_fd` if this is the first request.
- Adjust verifier time accounting to multi-rounds analysis.
- Minor cleanups: make zext/hi32 optimization read flags from `env`.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/linux/bpf_verifier.h |   3 +
 kernel/bpf/syscall.c         |   2 +
 kernel/bpf/verifier.c        | 113 +++++++++++++++++++++++++++++++++--
 3 files changed, 112 insertions(+), 6 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 05e8e3feea30..67eac7b2778e 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -774,6 +774,7 @@ struct bpf_verifier_env {
 	bool strict_alignment;		/* perform strict pointer alignment checks */
 	bool test_state_freq;		/* test verifier with different pruning frequency */
 	bool test_reg_invariants;	/* fail verification on register invariants violations */
+	bool test_rnd_hi32;		/* randomize high 32-bit to test subreg def/use */
 	struct bpf_verifier_state *cur_state; /* current verifier state */
 	/* Search pruning optimization, array of list_heads for
 	 * lists of struct bpf_verifier_state_list.
@@ -867,6 +868,8 @@ struct bpf_verifier_env {
 	u32 scc_cnt;
 	struct bpf_iarray *succ;
 	struct bcf_refine_state bcf;
+	/* The subprog being verified. */
+	u32 subprog;
 };
 
 static inline struct bpf_func_info_aux *subprog_aux(struct bpf_verifier_env *env, int subprog)
diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
index 5968b74ed7b2..97914494bd18 100644
--- a/kernel/bpf/syscall.c
+++ b/kernel/bpf/syscall.c
@@ -3096,6 +3096,8 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
 
 	/* run eBPF verifier */
 	err = bpf_check(&prog, attr, uattr, uattr_size);
+	if (prog->aux->bcf_requested)
+		return err;
 	if (err < 0)
 		goto free_used_maps;
 
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 22a068bfd0f2..3b631cea827e 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -15,6 +15,8 @@
 #include <linux/filter.h>
 #include <net/netlink.h>
 #include <linux/file.h>
+#include <linux/anon_inodes.h>
+#include <linux/fdtable.h>
 #include <linux/vmalloc.h>
 #include <linux/stringify.h>
 #include <linux/bsearch.h>
@@ -636,6 +638,11 @@ static void mark_bcf_requested(struct bpf_verifier_env *env)
 	env->prog->aux->bcf_requested = true;
 }
 
+static void unmark_bcf_requested(struct bpf_verifier_env *env)
+{
+	env->prog->aux->bcf_requested = false;
+}
+
 static int bcf_alloc_expr(struct bpf_verifier_env *env, u32 cnt)
 {
 	struct bcf_refine_state *bcf = &env->bcf;
@@ -22036,8 +22043,7 @@ static int opt_remove_nops(struct bpf_verifier_env *env)
 	return 0;
 }
 
-static int opt_subreg_zext_lo32_rnd_hi32(struct bpf_verifier_env *env,
-					 const union bpf_attr *attr)
+static int opt_subreg_zext_lo32_rnd_hi32(struct bpf_verifier_env *env)
 {
 	struct bpf_insn *patch;
 	/* use env->insn_buf as two independent buffers */
@@ -22049,7 +22055,7 @@ static int opt_subreg_zext_lo32_rnd_hi32(struct bpf_verifier_env *env,
 	struct bpf_prog *new_prog;
 	bool rnd_hi32;
 
-	rnd_hi32 = attr->prog_flags & BPF_F_TEST_RND_HI32;
+	rnd_hi32 = env->test_rnd_hi32;
 	zext_patch[1] = BPF_ZEXT_REG(0);
 	rnd_hi32_patch[1] = BPF_ALU64_IMM(BPF_MOV, BPF_REG_AX, 0);
 	rnd_hi32_patch[2] = BPF_ALU64_IMM(BPF_LSH, BPF_REG_AX, 32);
@@ -24233,7 +24239,7 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 	ret = do_check(env);
 
 	/* Invoked by bcf_track(), just return. */
-	if (env->bcf.tracking)
+	if (env->bcf.tracking || bcf_requested(env))
 		return ret;
 out:
 	if (!ret && pop_log)
@@ -24573,6 +24579,7 @@ static int do_check_subprogs(struct bpf_verifier_env *env)
 		if (!sub_aux->called || sub_aux->verified)
 			continue;
 
+		env->subprog = i;
 		env->insn_idx = env->subprog_info[i].start;
 		WARN_ON_ONCE(env->insn_idx == 0);
 		ret = do_check_common(env, i);
@@ -25766,6 +25773,85 @@ static int compute_scc(struct bpf_verifier_env *env)
 	return err;
 }
 
+static int bcf_release(struct inode *inode, struct file *filp)
+{
+	struct bpf_verifier_env *env = filp->private_data;
+
+	if (!env)
+		return 0;
+
+	free_states(env);
+	kvfree(env->explored_states);
+
+	if (!env->prog->aux->used_maps)
+		release_maps(env);
+	if (!env->prog->aux->used_btfs)
+		release_btfs(env);
+	bpf_prog_put(env->prog);
+
+	module_put(env->attach_btf_mod);
+	vfree(env->insn_aux_data);
+	bpf_stack_liveness_free(env);
+	kvfree(env->cfg.insn_postorder);
+	kvfree(env->scc_info);
+	kvfree(env->succ);
+	kvfree(env->bcf.exprs);
+	kvfree(env);
+	filp->private_data = NULL;
+	return 0;
+}
+
+static const struct file_operations bcf_fops = {
+	.release = bcf_release,
+};
+
+static int do_request_bcf(struct bpf_verifier_env *env, union bpf_attr *attr,
+			  bpfptr_t uattr)
+{
+	bpfptr_t bcf_buf = make_bpfptr(attr->bcf_buf, uattr.is_kernel);
+	int ret, bcf_fd = -1, flags = BCF_F_PROOF_REQUESTED;
+	struct bcf_refine_state *bcf = &env->bcf;
+	u32 sz, sz_off, expr_sz;
+
+	/* All exprs, followed by path_cond and refine_cond. */
+	expr_sz = bcf->expr_cnt * sizeof(struct bcf_expr);
+	sz = expr_sz + sizeof(bcf->path_cond) + sizeof(bcf->refine_cond);
+	sz_off = offsetof(union bpf_attr, bcf_buf_true_size);
+
+	ret = -EFAULT;
+	if (copy_to_bpfptr_offset(uattr, sz_off, &sz, sizeof(sz)))
+		return ret;
+	if (sz > attr->bcf_buf_size)
+		return -ENOSPC;
+
+	if (copy_to_bpfptr_offset(bcf_buf, 0, bcf->exprs, expr_sz) ||
+	    copy_to_bpfptr_offset(bcf_buf, expr_sz, &bcf->path_cond,
+				  sizeof(u32)) ||
+	    copy_to_bpfptr_offset(bcf_buf, expr_sz + sizeof(u32),
+				  &bcf->refine_cond, sizeof(u32)))
+		return ret;
+
+	if (copy_to_bpfptr_offset(uattr, offsetof(union bpf_attr, bcf_flags),
+				  &flags, sizeof(flags)))
+		return ret;
+
+	/* Allocate fd if first request. */
+	if (!(attr->bcf_flags & BCF_F_PROOF_PROVIDED)) {
+		bcf_fd = anon_inode_getfd("bcf", &bcf_fops, env,
+					  O_RDONLY | O_CLOEXEC);
+		if (bcf_fd < 0)
+			return bcf_fd;
+		if (copy_to_bpfptr_offset(uattr,
+					  offsetof(union bpf_attr, bcf_fd),
+					  &bcf_fd, sizeof(bcf_fd))) {
+			close_fd(bcf_fd);
+			return ret;
+		}
+	}
+
+	return 0;
+}
+
 int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u32 uattr_size)
 {
 	u64 start_time = ktime_get_ns();
@@ -25846,6 +25932,7 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	if (is_priv)
 		env->test_state_freq = attr->prog_flags & BPF_F_TEST_STATE_FREQ;
 	env->test_reg_invariants = attr->prog_flags & BPF_F_TEST_REG_INVARIANTS;
+	env->test_rnd_hi32 = attr->prog_flags & BPF_F_TEST_RND_HI32;
 
 	env->explored_states = kvcalloc(state_htab_size(env),
 				       sizeof(struct list_head),
@@ -25915,10 +26002,24 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	ret = do_check_main(env);
 	ret = ret ?: do_check_subprogs(env);
 
+	if (ret && bcf_requested(env)) {
+		u64 vtime = ktime_get_ns() - start_time;
+
+		env->verification_time += vtime;
+		if (do_request_bcf(env, attr, uattr) == 0)
+			return ret;
+
+		unmark_bcf_requested(env);
+		env->verification_time -= vtime;
+	}
+
 	if (ret == 0 && bpf_prog_is_offloaded(env->prog->aux))
 		ret = bpf_prog_offload_finalize(env);
 
 skip_full_check:
+	/* If bcf_requested(), the last state is preserved, free now. */
+	if (env->cur_state)
+		free_states(env);
 	kvfree(env->explored_states);
 
 	/* might decrease stack depth, keep it before passes that
@@ -25957,7 +26058,7 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	 * insns could be handled correctly.
 	 */
 	if (ret == 0 && !bpf_prog_is_offloaded(env->prog->aux)) {
-		ret = opt_subreg_zext_lo32_rnd_hi32(env, attr);
+		ret = opt_subreg_zext_lo32_rnd_hi32(env);
 		env->prog->aux->verifier_zext = bpf_jit_needs_zext() ? !ret
 								     : false;
 	}
@@ -25965,7 +26066,7 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	if (ret == 0)
 		ret = fixup_call_args(env);
 
-	env->verification_time = ktime_get_ns() - start_time;
+	env->verification_time += ktime_get_ns() - start_time;
 	print_verification_stats(env);
 	env->prog->aux->verified_insns = env->insn_processed;
 
-- 
2.34.1

[PATCH RFC 16/17] bpf: Resume verifier env and check proof

[Hao Sun]

Add the resume path for proof-based refinement and integrate proof check
into the verifier flow.

- Userspace sets `BCF_F_PROOF_PROVIDED`, passes the saved `bcf_fd` and a proof
  in `bcf_buf`. bpf_prog_load() detects resume, swaps to verifier path without
  building a new prog, and calls bpf_check() with `prog = NULL`.

- In bpf_check(), fetch the saved env from `bcf_fd`, ensure it’s a BCF file and
  not already in use (`bcf.in_use`), and mark it in-use.

- `resume_env()`: determine which condition to check (default `refine_cond`; if
  `BCF_F_PROOF_PATH_UNREACHABLE` is set, use `path_cond` and mark
  `path_unreachable` to skip to exit on the next insn). Copy the proof from
  userspace and call `bcf_check_proof()` with the saved expression arena and
  condition id.

- Resume verification: skip re-initialization if `env->cur_state` exists;
  analyze only the subprog recorded at request time; continue with the refined
  `cur_state` and finish normal verification.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 include/linux/bpf_verifier.h |  2 +
 kernel/bpf/syscall.c         |  6 ++-
 kernel/bpf/verifier.c        | 94 +++++++++++++++++++++++++++++++++---
 3 files changed, 94 insertions(+), 8 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index 67eac7b2778e..219e211195fc 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -745,6 +745,7 @@ struct bcf_refine_state {
 
 	bool available; /* if bcf_buf is provided. */
 	bool tracking; /* In bcf_track(). */
+	atomic_t in_use; /* The current env is in use. */
 	struct bcf_expr *exprs;
 	u32 expr_size;
 	u32 expr_cnt;
@@ -758,6 +759,7 @@ struct bcf_refine_state {
 	int checked_off;
 	int checked_sz;
 	bool access_checked;
+	bool path_unreachable;
 };
 
 /* single container for all structs
diff --git a/kernel/bpf/syscall.c b/kernel/bpf/syscall.c
index 97914494bd18..53ed868aa20c 100644
--- a/kernel/bpf/syscall.c
+++ b/kernel/bpf/syscall.c
@@ -2881,7 +2881,8 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
 			return -EINVAL;
 		/* The resumed analysis must only uses the old, first attr. */
 		memset(attr, 0, offsetof(union bpf_attr, bcf_buf));
-		return -ENOTSUPP;
+		prog = NULL;
+		goto verifier_check;
 	}
 
 	if (attr->bcf_fd || attr->bcf_buf_true_size || attr->bcf_flags)
@@ -3094,9 +3095,10 @@ static int bpf_prog_load(union bpf_attr *attr, bpfptr_t uattr, u32 uattr_size)
 	if (err)
 		goto free_prog_sec;
 
+verifier_check:
 	/* run eBPF verifier */
 	err = bpf_check(&prog, attr, uattr, uattr_size);
-	if (prog->aux->bcf_requested)
+	if (!prog || prog->aux->bcf_requested)
 		return err;
 	if (err < 0)
 		goto free_used_maps;
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 3b631cea827e..fb672c9cc7cd 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -33,6 +33,7 @@
 #include <net/xdp.h>
 #include <linux/trace_events.h>
 #include <linux/kallsyms.h>
+#include <linux/bcf_checker.h>
 
 #include "disasm.h"
 
@@ -20927,6 +20928,11 @@ static int do_check(struct bpf_verifier_env *env)
 		insn = &insns[env->insn_idx];
 		insn_aux = &env->insn_aux_data[env->insn_idx];
 
+		if (env->bcf.path_unreachable) {
+			env->bcf.path_unreachable = false;
+			goto process_bpf_exit;
+		}
+
 		if (++env->insn_processed > BPF_COMPLEXITY_LIMIT_INSNS) {
 			verbose(env,
 				"BPF program is too large. Processed %d insn\n",
@@ -24123,6 +24129,9 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 	struct bpf_reg_state *regs;
 	int ret, i;
 
+	if (env->cur_state)
+		goto skip_init;
+
 	env->prev_insn_idx = -1;
 	env->prev_linfo = NULL;
 	env->pass_cnt++;
@@ -24236,6 +24245,7 @@ static int do_check_common(struct bpf_verifier_env *env, int subprog)
 							  acquire_reference(env, 0) : 0;
 	}
 
+skip_init:
 	ret = do_check(env);
 
 	/* Invoked by bcf_track(), just return. */
@@ -24571,7 +24581,9 @@ static int do_check_subprogs(struct bpf_verifier_env *env)
 
 again:
 	new_cnt = 0;
-	for (i = 1; i < env->subprog_cnt; i++) {
+	/* env->cur_state indicates the resume mode, check the last subprog */
+	i = env->cur_state ? env->subprog : 1;
+	for (; i < env->subprog_cnt; i++) {
 		if (!subprog_is_global(env, i))
 			continue;
 
@@ -24580,8 +24592,10 @@ static int do_check_subprogs(struct bpf_verifier_env *env)
 			continue;
 
 		env->subprog = i;
-		env->insn_idx = env->subprog_info[i].start;
-		WARN_ON_ONCE(env->insn_idx == 0);
+		if (!env->cur_state) {
+			env->insn_idx = env->subprog_info[i].start;
+			WARN_ON_ONCE(env->insn_idx == 0);
+		}
 		ret = do_check_common(env, i);
 		if (ret) {
 			return ret;
@@ -24611,7 +24625,10 @@ static int do_check_main(struct bpf_verifier_env *env)
 {
 	int ret;
 
-	env->insn_idx = 0;
+	if (env->subprog)
+		return 0;
+	if (!env->cur_state)
+		env->insn_idx = 0;
 	ret = do_check_common(env, 0);
 	if (!ret)
 		env->prog->aux->stack_depth = env->subprog_info[0].stack_depth;
@@ -25852,13 +25869,45 @@ static int do_request_bcf(struct bpf_verifier_env *env, union bpf_attr *attr,
 	return 0;
 }
 
+static int resume_env(struct bpf_verifier_env *env, union bpf_attr *attr,
+		      bpfptr_t uattr)
+{
+	bpfptr_t proof;
+	int cond, err;
+
+	unmark_bcf_requested(env);
+
+	cond = env->bcf.refine_cond;
+	if (attr->bcf_flags & BCF_F_PROOF_PATH_UNREACHABLE) {
+		cond = env->bcf.path_cond;
+		env->bcf.path_unreachable = true;
+	}
+	if (cond < 0)
+		return -EINVAL;
+
+	proof = make_bpfptr(attr->bcf_buf, uattr.is_kernel);
+	err = bcf_check_proof(env->bcf.exprs, cond, proof,
+			      attr->bcf_buf_true_size,
+			      (void *)bpf_verifier_vlog, env->log.level,
+			      &env->log);
+	if (err)
+		return err;
+
+	/* Drop the last history entry */
+	if (is_jmp_point(env, env->insn_idx))
+		env->cur_state->jmp_history_cnt--;
+
+	return 0;
+}
+
 int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u32 uattr_size)
 {
 	u64 start_time = ktime_get_ns();
 	struct bpf_verifier_env *env;
 	int i, len, ret = -EINVAL, err;
 	u32 log_true_size;
-	bool is_priv;
+	bool is_priv, resume;
+	struct fd bcf_fd;
 
 	BTF_TYPE_EMIT(enum bpf_features);
 
@@ -25866,6 +25915,24 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	if (ARRAY_SIZE(bpf_verifier_ops) == 0)
 		return -EINVAL;
 
+	resume = !!(attr->bcf_flags & BCF_F_PROOF_PROVIDED);
+	if (resume) {
+		struct file *f;
+
+		bcf_fd = fdget(attr->bcf_fd);
+		f = fd_file(bcf_fd);
+		if (!f)
+			return -EBADF;
+		env = f->private_data;
+		if (f->f_op != &bcf_fops ||
+		    atomic_cmpxchg(&env->bcf.in_use, 0, 1)) {
+			fdput(bcf_fd);
+			return -EINVAL;
+		}
+		is_priv = env->bpf_capable;
+		goto verifier_check;
+	}
+
 	/* 'struct bpf_verifier_env' can be global, but since it's not small,
 	 * allocate/free it every time bpf_check() is called
 	 */
@@ -25999,6 +26066,12 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	if (ret < 0)
 		goto skip_full_check;
 
+verifier_check:
+	if (resume) {
+		ret = resume_env(env, attr, uattr);
+		if (ret)
+			goto skip_full_check;
+	}
 	ret = do_check_main(env);
 	ret = ret ?: do_check_subprogs(env);
 
@@ -26006,8 +26079,13 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 		u64 vtime = ktime_get_ns() - start_time;
 
 		env->verification_time += vtime;
-		if (do_request_bcf(env, attr, uattr) == 0)
+		if (do_request_bcf(env, attr, uattr) == 0) {
+			if (resume) {
+				atomic_set(&env->bcf.in_use, 0);
+				fdput(bcf_fd);
+			}
 			return ret;
+		}
 
 		unmark_bcf_requested(env);
 		env->verification_time -= vtime;
@@ -26017,6 +26095,10 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 		ret = bpf_prog_offload_finalize(env);
 
 skip_full_check:
+	if (resume) {
+		fd_file(bcf_fd)->private_data = NULL;
+		fdput(bcf_fd);
+	}
 	/* If bcf_requested(), the last state is preserved, free now. */
 	if (env->cur_state)
 		free_states(env);
-- 
2.34.1

[PATCH RFC 17/17] bpf: Enable bcf for priv users

[Hao Sun]

Enable bcf when bcf_buf is provided and is_priv.

Signed-off-by: Hao Sun <hao.sun@inf.ethz.ch>
---
 kernel/bpf/verifier.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index fb672c9cc7cd..d48357bac9f3 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -25961,6 +25961,7 @@ int bpf_check(struct bpf_prog **prog, union bpf_attr *attr, bpfptr_t uattr, __u3
 	env->bypass_spec_v1 = bpf_bypass_spec_v1(env->prog->aux->token);
 	env->bypass_spec_v4 = bpf_bypass_spec_v4(env->prog->aux->token);
 	env->bpf_capable = is_priv = bpf_token_capable(env->prog->aux->token, CAP_BPF);
+	env->bcf.available = is_priv && attr->bcf_buf_size;
 
 	bpf_get_btf_vmlinux();
 
-- 
2.34.1