Re: [PATCH v2 bpf-next 4/6] bpf: Simulate branches to prune based on range violations

[Mykyta Yatsenko <mykyta.yatsenko5@gmail.com>]

Paul Chaignon <paul.chaignon@gmail.com> writes:

> From: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
>
> 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 (formally verified). 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 mis-detected 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.
>
> 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>
> ---
>  kernel/bpf/verifier.c | 84 +++++++++++++++++++++++++------------------
>  1 file changed, 49 insertions(+), 35 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 8d7ad5f21ed6..0b4f622efec1 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -16717,11 +16717,48 @@ 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 both branches being
> + * taken using regs_refine_cond_op. Because regs_refine_cond_op is sound when
> + * the branch is taken, if it produces ill-formed register bounds, it must mean
> + * that the branch is dead.
> + */
Sorry for being nit-picky, could you please use kernel style comment style +
maybe reword it a little bit, instead of:

/*
 * Because regs_refine_cond_op is sound when
 * the branch is taken, if it produces ill-formed register bounds, it must mean
 * that the branch is dead.
 */
Something like:
/*
 * 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);
This is probably more related to patch 2: is it necessary to have both
true/false_reg1/2 pairs, it looks like we process false branch before
the true branch and they never intersect, don't they? So it worth
removing a pair of bpf_reg_states from env?
> +	/* 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;
> @@ -16873,7 +16910,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)
> @@ -16944,8 +16981,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);
> @@ -16983,7 +17020,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.
> @@ -17074,8 +17111,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.
> @@ -17182,34 +17219,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");
> @@ -17595,7 +17609,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.
> @@ -17659,7 +17673,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;
>  
> -- 
> 2.43.0