bpf: Save pruning point states in oracle

This patch saves information on the verifier states, at each pruning
point, into bpf_insn_aux_data, for use by the BPF oracle. The verifier
is already saving states into explored_states for state pruning, but we
can't reuse it for the oracle.

For state pruning, we only save a subset of all states at each pruning
point. Specifically, we will only save a new state if we've seen at
least 8 instructions and 2 BPF_JMPs since we last saved a state. For the
oracle, we will use the saved information to ensure that concrete values
match at least one verifier state. If we are missing states, we will
have false positives.

This patch therefore saves information on verifier states at every
pruning point, regardless of existing heuristics. A later patch will
limit this behavior to CONFIG_BPF_ORACLE.

At the moment, the oracle only saves information on the type and ranges
(in case of scalars) of registers. No information is kept for stack
slots. More checks can be added later.

Signed-off-by: Paul Chaignon <[email protected]>

Author: pchaigno

include/linux/bpf_verifier.h

@@ -485,6 +485,30 @@ struct bpf_verifier_state_list {
 	u32 in_free_list:1;
 };
 
+struct bpf_reg_oracle_state {
+	bool scalar;
+	bool ptr_not_null;
+
+	struct tnum var_off;
+	s64 smin_value;
+	s64 smax_value;
+	u64 umin_value;
+	u64 umax_value;
+	s32 s32_min_value;
+	s32 s32_max_value;
+	u32 u32_min_value;
+	u32 u32_max_value;
+};
+
+struct bpf_oracle_state {
+	struct bpf_reg_oracle_state regs[MAX_BPF_REG - 1];
+};
+
+struct bpf_oracle_state_list {
+	struct bpf_oracle_state state;
+	struct list_head node;
+};
+
 struct bpf_loop_inline_state {
 	unsigned int initialized:1; /* set to true upon first entry */
 	unsigned int fit_for_inline:1; /* true if callback function is the same
@@ -551,6 +575,7 @@ struct bpf_insn_aux_data {
 	};
 	struct bpf_iarray *jt;	/* jump table for gotox or bpf_tailcall call instruction */
 	struct btf_struct_meta *kptr_struct_meta;
+	struct list_head *oracle_states;
 	u64 map_key_state; /* constant (32 bit) key tracking for maps */
 	int ctx_field_size; /* the ctx field size for load insn, maybe 0 */
 	u32 seen; /* this insn was processed by the verifier at env->pass_cnt */
@@ -1060,11 +1085,18 @@ static inline bool insn_is_gotox(struct bpf_insn *insn)
 	       BPF_SRC(insn->code) == BPF_X;
 }
 
+static inline struct bpf_insn_aux_data *cur_aux(const struct bpf_verifier_env *env)
+{
+	return &env->insn_aux_data[env->insn_idx];
+}
+
 const char *reg_type_str(struct bpf_verifier_env *env, enum bpf_reg_type type);
 const char *dynptr_type_str(enum bpf_dynptr_type type);
 const char *iter_type_str(const struct btf *btf, u32 btf_id);
 const char *iter_state_str(enum bpf_iter_state state);
 
+bool reg_not_null(const struct bpf_reg_state *reg);
+
 void print_verifier_state(struct bpf_verifier_env *env, const struct bpf_verifier_state *vstate,
 			  u32 frameno, bool print_all);
 void print_insn_state(struct bpf_verifier_env *env, const struct bpf_verifier_state *vstate,
@@ -1087,4 +1119,6 @@ int bpf_live_stack_query_init(struct bpf_verifier_env *env, struct bpf_verifier_
 bool bpf_stack_slot_alive(struct bpf_verifier_env *env, u32 frameno, u32 spi);
 void bpf_reset_live_stack_callchain(struct bpf_verifier_env *env);
 
+int save_state_in_oracle(struct bpf_verifier_env *env, int insn_idx);
+
 #endif /* _LINUX_BPF_VERIFIER_H */

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 oracle.o log.o token.o liveness.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 bpf_insn_array.o

kernel/bpf/oracle.c

@@ -0,0 +1,63 @@
+// SPDX-License-Identifier: GPL-2.0-only
+/*
+ * This file implements a test oracle for the verifier. When the oracle is enabled, the verifier
+ * saves information on variables at regular points throughout the program. This information is
+ * then compared at runtime with the concrete values to ensure that the verifier's information is
+ * correct.
+ */
+
+#include <linux/bpf_verifier.h>
+
+static void convert_oracle_state(struct bpf_verifier_state *istate, struct bpf_oracle_state *ostate)
+{
+	struct bpf_func_state *frame = istate->frame[istate->curframe];
+	struct bpf_reg_oracle_state *oreg;
+	struct bpf_reg_state *ireg;
+	int i;
+
+	/* No need to check R10 with the oracle. */
+	for (i = 0; i < MAX_BPF_REG - 1; i++) {
+		ireg = &frame->regs[i];
+		oreg = &ostate->regs[i];
+
+		oreg->scalar = ireg->type == SCALAR_VALUE;
+		oreg->ptr_not_null = reg_not_null(ireg);
+
+		oreg->var_off = ireg->var_off;
+		oreg->smin_value = ireg->smin_value;
+		oreg->smax_value = ireg->smax_value;
+		oreg->umin_value = ireg->umin_value;
+		oreg->umax_value = ireg->umax_value;
+		oreg->s32_min_value = ireg->s32_min_value;
+		oreg->s32_max_value = ireg->s32_max_value;
+		oreg->u32_min_value = ireg->u32_min_value;
+		oreg->u32_max_value = ireg->u32_max_value;
+	}
+}
+
+int save_state_in_oracle(struct bpf_verifier_env *env, int insn_idx)
+{
+	struct bpf_verifier_state *cur = env->cur_state;
+	struct bpf_insn_aux_data *aux = cur_aux(env);
+	struct bpf_oracle_state_list *new_sl;
+
+	if (env->subprog_cnt > 1)
+		/* Skip the oracle if subprogs are used. */
+		return 0;
+
+	if (!aux->oracle_states) {
+		aux->oracle_states = kmalloc(sizeof(*aux->oracle_states), GFP_KERNEL_ACCOUNT);
+		if (!aux->oracle_states)
+			return -ENOMEM;
+
+		INIT_LIST_HEAD(aux->oracle_states);
+	}
+
+	new_sl = kzalloc(sizeof(*new_sl), GFP_KERNEL_ACCOUNT);
+	if (!new_sl)
+		return -ENOMEM;
+	convert_oracle_state(cur, &new_sl->state);
+	list_add(&new_sl->node, aux->oracle_states);
+
+	return 0;
+}

kernel/bpf/verifier.c

@@ -394,7 +394,7 @@ static void verbose_invalid_scalar(struct bpf_verifier_env *env,
 	verbose(env, " should have been in [%d, %d]\n", range.minval, range.maxval);
 }
 
-static bool reg_not_null(const struct bpf_reg_state *reg)
+bool reg_not_null(const struct bpf_reg_state *reg)
 {
 	enum bpf_reg_type type;
 
@@ -11398,11 +11398,6 @@ static int check_get_func_ip(struct bpf_verifier_env *env)
 	return -ENOTSUPP;
 }
 
-static struct bpf_insn_aux_data *cur_aux(const struct bpf_verifier_env *env)
-{
-	return &env->insn_aux_data[env->insn_idx];
-}
-
 static bool loop_flag_is_zero(struct bpf_verifier_env *env)
 {
 	struct bpf_reg_state *regs = cur_regs(env);
@@ -20508,6 +20503,10 @@ static int do_check(struct bpf_verifier_env *env)
 		state->insn_idx = env->insn_idx;
 
 		if (is_prune_point(env, env->insn_idx)) {
+			err = save_state_in_oracle(env, env->insn_idx);
+			if (err < 0)
+				return err;
+
 			err = is_state_visited(env, env->insn_idx);
 			if (err < 0)
 				return err;