* [PATCH RFC 01/17] bpf: Add BCF expr and proof rule definitions
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 02/17] bpf: Add bcf_checker top-level workflow Hao Sun
` (15 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 02/17] bpf: Add bcf_checker top-level workflow
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
2025-11-06 12:52 ` [PATCH RFC 01/17] bpf: Add BCF expr and proof rule definitions Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 03/17] bpf: Add UAPI fields for BCF proof interaction Hao Sun
` (14 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 03/17] bpf: Add UAPI fields for BCF proof interaction
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
2025-11-06 12:52 ` [PATCH RFC 01/17] bpf: Add BCF expr and proof rule definitions Hao Sun
2025-11-06 12:52 ` [PATCH RFC 02/17] bpf: Add bcf_checker top-level workflow Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 04/17] bpf: Add top-level workflow of bcf_refine() Hao Sun
` (13 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 04/17] bpf: Add top-level workflow of bcf_refine()
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (2 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 03/17] bpf: Add UAPI fields for BCF proof interaction Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 05/17] bpf: Add top-level workflow of bcf_track() Hao Sun
` (12 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 05/17] bpf: Add top-level workflow of bcf_track()
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (3 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 04/17] bpf: Add top-level workflow of bcf_refine() Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 06/17] bpf: Add bcf_match_path() to follow the path suffix Hao Sun
` (11 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 06/17] bpf: Add bcf_match_path() to follow the path suffix
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (4 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 05/17] bpf: Add top-level workflow of bcf_track() Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 07/17] bpf: Add bcf_expr management and binding Hao Sun
` (10 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 07/17] bpf: Add bcf_expr management and binding
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (5 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 06/17] bpf: Add bcf_match_path() to follow the path suffix Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 08/17] bpf: Track mov and signed extension Hao Sun
` (9 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 08/17] bpf: Track mov and signed extension
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (6 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 07/17] bpf: Add bcf_expr management and binding Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 09/17] bpf: Track alu operations in bcf_track() Hao Sun
` (8 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 09/17] bpf: Track alu operations in bcf_track()
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (7 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 08/17] bpf: Track mov and signed extension Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 10/17] bpf: Add bcf_alu() 32bits optimization Hao Sun
` (7 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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 = ®s[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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 10/17] bpf: Add bcf_alu() 32bits optimization
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (8 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 09/17] bpf: Track alu operations in bcf_track() Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 11/17] bpf: Track stack spill/fill in bcf_track() Hao Sun
` (6 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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 = ®s[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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 11/17] bpf: Track stack spill/fill in bcf_track()
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (9 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 10/17] bpf: Add bcf_alu() 32bits optimization Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 12/17] bpf: Track path constraint Hao Sun
` (5 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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(®s[value_regno], size);
else
coerce_reg_to_size_sx(®s[value_regno], size);
+
+ if (env->bcf.tracking && regs[value_regno].bcf_expr >= 0)
+ err = bcf_mov(env, ®s[value_regno],
+ ®s[value_regno], size * 8, false,
+ is_ldsx);
}
return err;
}
--
2.34.1
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 12/17] bpf: Track path constraint
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (10 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 11/17] bpf: Track stack spill/fill in bcf_track() Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 13/17] bpf: Skip state pruning for the parent states Hao Sun
` (4 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 13/17] bpf: Skip state pruning for the parent states
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (11 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 12/17] bpf: Track path constraint Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 14/17] bpf: Add mem access bound refinement Hao Sun
` (3 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 14/17] bpf: Add mem access bound refinement
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (12 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 13/17] bpf: Skip state pruning for the parent states Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 15/17] bpf: Preserve verifier_env and request BCF Hao Sun
` (2 subsequent siblings)
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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, ®s[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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 15/17] bpf: Preserve verifier_env and request BCF
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (13 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 14/17] bpf: Add mem access bound refinement Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 16/17] bpf: Resume verifier env and check proof Hao Sun
2025-11-06 12:52 ` [PATCH RFC 17/17] bpf: Enable bcf for priv users Hao Sun
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 16/17] bpf: Resume verifier env and check proof
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (14 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 15/17] bpf: Preserve verifier_env and request BCF Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
2025-11-06 12:52 ` [PATCH RFC 17/17] bpf: Enable bcf for priv users Hao Sun
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread* [PATCH RFC 17/17] bpf: Enable bcf for priv users
2025-11-06 12:52 [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement Hao Sun
` (15 preceding siblings ...)
2025-11-06 12:52 ` [PATCH RFC 16/17] bpf: Resume verifier env and check proof Hao Sun
@ 2025-11-06 12:52 ` Hao Sun
16 siblings, 0 replies; 18+ messages in thread
From: Hao Sun @ 2025-11-06 12:52 UTC (permalink / raw)
To: bpf
Cc: ast, daniel, andrii, eddyz87, john.fastabend, martin.lau, song,
yonghong.song, linux-kernel, sunhao.th, 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
^ permalink raw reply related [flat|nested] 18+ messages in thread