bpf: Simulate branches to prune based on range violations

This patch fixes the invariant violations that can happen after we
refine ranges & tnum based on an incorrectly-detected branch condition.
For example, the branch is always true, but we miss it in
is_branch_taken; we then refine based on the branch being false and end
up with incoherent ranges (e.g. umax < umin).

To avoid this, we can simulate the refinement on both branches. More
specifically, this patch simulates both branches taken using
regs_refine_cond_op and reg_bounds_sync. If the resulting register
states are ill-formed on one of the branches, is_branch_taken can mark
that branch as "never taken".

On a more formal note, we can deduce a branch is not taken when
regs_refine_cond_op or reg_bounds_sync returns an ill-formed state
because the branch operators are sound (verified with Agni [1]).
Soundness means that the verifier is guaranteed to produce sound
outputs on the taken branches. On the non-taken branch (explored
because of imprecision in the bounds), the verifier is free to produce
any output. We use ill-formedness as a signal that the branch is dead
and prune that branch.

This patch moves the refinement logic for both branches from
reg_set_min_max to their own function, simulate_both_branches_taken,
which is called from is_scalar_branch_taken. As a result,
reg_set_min_max now only runs sanity checks and has been renamed to
reg_bounds_sanity_check_branches to reflect that.

We have had five patches fixing specific cases of invariant violations
in the past, all added with selftests:
- commit fbc7aef517d8 ("bpf: Fix u32/s32 bounds when ranges cross
  min/max boundary")
- commit efc11a667878 ("bpf: Improve bounds when tnum has a single
  possible value")
- commit f41345f47fb2 ("bpf: Use tnums for JEQ/JNE is_branch_taken
  logic")
- commit 00bf8d0c6c9b ("bpf: Improve bounds when s64 crosses sign
  boundary")
- commit 6279846b9b25 ("bpf: Forget ranges when refining tnum after
  JSET")

To confirm that this patch addresses all invariant violations, we have
also reverted those five commits and verified that their related
selftests don't cause any invariant violation warnings anymore. Those
selftests still fail but only because of misdetected branches or
less-precise bounds than expected. This demonstrates that the current
patch is enough to avoid the invariant violation warning AND that the
previous five patches are still useful to improve branch detection.

In addition to the selftests, this change was also tested with the
Cilium complexity test suite: all programs were successfully loaded and
it didn't change the number of processed instructions.

Link: https://github.com/bpfverif/agni
Reported-by: syzbot+c950cc277150935cc0b5@syzkaller.appspotmail.com
Closes: https://syzkaller.appspot.com/bug?extid=c950cc277150935cc0b5
Co-developed-by: Paul Chaignon <paul.chaignon@gmail.com>
Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Acked-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/a166b54a3cbbbdbcdf8a87f53045f1097176218b.1775142354.git.paul.chaignon@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 8215355f6be003a313b23cc4854a8396ddb3712e..a431b7d50e1b831ebe503c3c90f86127782722c5 100644 (file)
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -16786,11 +16786,50 @@ static void find_good_pkt_pointers(struct bpf_verifier_state *vstate,
        }));
 }
 
+static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
+                               u8 opcode, bool is_jmp32);
+static u8 rev_opcode(u8 opcode);
+
+/*
+ * Learn more information about live branches by simulating refinement on both branches.
+ * regs_refine_cond_op() is sound, so producing ill-formed register bounds for the branch means
+ * that branch is dead.
+ */
+static int simulate_both_branches_taken(struct bpf_verifier_env *env, u8 opcode, bool is_jmp32)
+{
+       /* Fallthrough (FALSE) branch */
+       regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
+       reg_bounds_sync(&env->false_reg1);
+       reg_bounds_sync(&env->false_reg2);
+       /*
+        * If there is a range bounds violation in *any* of the abstract values in either
+        * reg_states in the FALSE branch (i.e. reg1, reg2), the FALSE branch must be dead. Only
+        * TRUE branch will be taken.
+        */
+       if (range_bounds_violation(&env->false_reg1) || range_bounds_violation(&env->false_reg2))
+               return 1;
+
+       /* Jump (TRUE) branch */
+       regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
+       reg_bounds_sync(&env->true_reg1);
+       reg_bounds_sync(&env->true_reg2);
+       /*
+        * If there is a range bounds violation in *any* of the abstract values in either
+        * reg_states in the TRUE branch (i.e. true_reg1, true_reg2), the TRUE branch must be dead.
+        * Only FALSE branch will be taken.
+        */
+       if (range_bounds_violation(&env->true_reg1) || range_bounds_violation(&env->true_reg2))
+               return 0;
+
+       /* Both branches are possible, we can't determine which one will be taken. */
+       return -1;
+}
+
 /*
  * <reg1> <op> <reg2>, currently assuming reg2 is a constant
  */
-static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
-                                 u8 opcode, bool is_jmp32)
+static int is_scalar_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
+                                 struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
 {
        struct tnum t1 = is_jmp32 ? tnum_subreg(reg1->var_off) : reg1->var_off;
        struct tnum t2 = is_jmp32 ? tnum_subreg(reg2->var_off) : reg2->var_off;
@@ -16942,7 +16981,7 @@ static int is_scalar_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_sta
                break;
        }
 
-       return -1;
+       return simulate_both_branches_taken(env, opcode, is_jmp32);
 }
 
 static int flip_opcode(u32 opcode)
@@ -17013,8 +17052,8 @@ static int is_pkt_ptr_branch_taken(struct bpf_reg_state *dst_reg,
  * -1 - unknown. Example: "if (reg1 < 5)" is unknown when register value
  *      range [0,10]
  */
-static int is_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg2,
-                          u8 opcode, bool is_jmp32)
+static int is_branch_taken(struct bpf_verifier_env *env, struct bpf_reg_state *reg1,
+                          struct bpf_reg_state *reg2, u8 opcode, bool is_jmp32)
 {
        if (reg_is_pkt_pointer_any(reg1) && reg_is_pkt_pointer_any(reg2) && !is_jmp32)
                return is_pkt_ptr_branch_taken(reg1, reg2, opcode);
@@ -17052,7 +17091,7 @@ static int is_branch_taken(struct bpf_reg_state *reg1, struct bpf_reg_state *reg
        }
 
        /* now deal with two scalars, but not necessarily constants */
-       return is_scalar_branch_taken(reg1, reg2, opcode, is_jmp32);
+       return is_scalar_branch_taken(env, reg1, reg2, opcode, is_jmp32);
 }
 
 /* Opcode that corresponds to a *false* branch condition.
@@ -17143,8 +17182,8 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
                        /* u32_min_value is not equal to 0xffffffff at this point,
                         * because otherwise u32_max_value is 0xffffffff as well,
                         * in such a case both reg1 and reg2 would be constants,
-                        * jump would be predicted and reg_set_min_max() won't
-                        * be called.
+                        * jump would be predicted and regs_refine_cond_op()
+                        * wouldn't be called.
                         *
                         * Same reasoning works for all {u,s}{min,max}{32,64} cases
                         * below.
@@ -17251,34 +17290,11 @@ static void regs_refine_cond_op(struct bpf_reg_state *reg1, struct bpf_reg_state
        }
 }
 
-/* Adjusts the register min/max values in the case that the dst_reg and
- * src_reg are both SCALAR_VALUE registers (or we are simply doing a BPF_K
- * check, in which case we have a fake SCALAR_VALUE representing insn->imm).
- * Technically we can do similar adjustments for pointers to the same object,
- * but we don't support that right now.
- */
-static int reg_set_min_max(struct bpf_verifier_env *env,
-                          u8 opcode, bool is_jmp32)
+/* Check for invariant violations on the registers for both branches of a condition */
+static int regs_bounds_sanity_check_branches(struct bpf_verifier_env *env)
 {
        int err;
 
-       /* If either register is a pointer, we can't learn anything about its
-        * variable offset from the compare (unless they were a pointer into
-        * the same object, but we don't bother with that).
-        */
-       if (env->false_reg1.type != SCALAR_VALUE || env->false_reg2.type != SCALAR_VALUE)
-               return 0;
-
-       /* fallthrough (FALSE) branch */
-       regs_refine_cond_op(&env->false_reg1, &env->false_reg2, rev_opcode(opcode), is_jmp32);
-       reg_bounds_sync(&env->false_reg1);
-       reg_bounds_sync(&env->false_reg2);
-
-       /* jump (TRUE) branch */
-       regs_refine_cond_op(&env->true_reg1, &env->true_reg2, opcode, is_jmp32);
-       reg_bounds_sync(&env->true_reg1);
-       reg_bounds_sync(&env->true_reg2);
-
        err = reg_bounds_sanity_check(env, &env->true_reg1, "true_reg1");
        err = err ?: reg_bounds_sanity_check(env, &env->true_reg2, "true_reg2");
        err = err ?: reg_bounds_sanity_check(env, &env->false_reg1, "false_reg1");
@@ -17670,7 +17686,7 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
        copy_register_state(&env->false_reg2, src_reg);
        copy_register_state(&env->true_reg1, dst_reg);
        copy_register_state(&env->true_reg2, src_reg);
-       pred = is_branch_taken(dst_reg, src_reg, opcode, is_jmp32);
+       pred = is_branch_taken(env, dst_reg, src_reg, opcode, is_jmp32);
        if (pred >= 0) {
                /* If we get here with a dst_reg pointer type it is because
                 * above is_branch_taken() special cased the 0 comparison.
@@ -17734,7 +17750,7 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
                return PTR_ERR(other_branch);
        other_branch_regs = other_branch->frame[other_branch->curframe]->regs;
 
-       err = reg_set_min_max(env, opcode, is_jmp32);
+       err = regs_bounds_sanity_check_branches(env);
        if (err)
                return err;