[PATCH bpf-next] bpf: Propagate memory bounds to registers in atomics w/ BPF_FETCH

[PATCH bpf-next] bpf: Propagate memory bounds to registers in atomics w/ BPF_FETCH

[Brendan Jackman]

When BPF_FETCH is set, atomic instructions load a value from memory
into a register. The current verifier code first checks via
check_mem_access whether we can access the memory, and then checks
via check_reg_arg whether we can write into the register.

For loads, check_reg_arg has the side-effect of marking the
register's value as unkonwn, and check_mem_access has the side effect
of propagating bounds from memory to the register.

Therefore with the current order, bounds information is thrown away,
but by simply reversing the order of check_reg_arg
vs. check_mem_access, we can instead propagate bounds smartly.

A simple test is added with an infinite loop that can only be proved
unreachable if this propagation is present.

Note that in the test, the memory value has to be written with two
instructions:

		BPF_MOV64_IMM(BPF_REG_0, 0),
		BPF_STX_MEM(BPF_DW, BPF_REG_10, BPF_REG_0, -8),

instead of one:

		BPF_ST_MEM(BPF_DW, BPF_REG_10, -8, 0),

Because BPF_ST_MEM doesn't seem to set the stack slot type to 0 when
storing an immediate.

Signed-off-by: Brendan Jackman <jackmanb@google.com>
---
 kernel/bpf/verifier.c                         | 32 +++++++++++--------
 .../selftests/bpf/verifier/atomic_bounds.c    | 18 +++++++++++
 2 files changed, 36 insertions(+), 14 deletions(-)
 create mode 100644 tools/testing/selftests/bpf/verifier/atomic_bounds.c

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 0f82d5d46e2c..0512695c70f4 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -3663,9 +3663,26 @@ static int check_atomic(struct bpf_verifier_env *env, int insn_idx, struct bpf_i
 		return -EACCES;
 	}
 
+	if (insn->imm & BPF_FETCH) {
+		if (insn->imm == BPF_CMPXCHG)
+			load_reg = BPF_REG_0;
+		else
+			load_reg = insn->src_reg;
+
+		/* check and record load of old value */
+		err = check_reg_arg(env, load_reg, DST_OP);
+		if (err)
+			return err;
+	} else {
+		/* This instruction accesses a memory location but doesn't
+		 * actually load it into a register.
+		 */
+		load_reg = -1;
+	}
+
 	/* check whether we can read the memory */
 	err = check_mem_access(env, insn_idx, insn->dst_reg, insn->off,
-			       BPF_SIZE(insn->code), BPF_READ, -1, true);
+			       BPF_SIZE(insn->code), BPF_READ, load_reg, true);
 	if (err)
 		return err;
 
@@ -3675,19 +3692,6 @@ static int check_atomic(struct bpf_verifier_env *env, int insn_idx, struct bpf_i
 	if (err)
 		return err;
 
-	if (!(insn->imm & BPF_FETCH))
-		return 0;
-
-	if (insn->imm == BPF_CMPXCHG)
-		load_reg = BPF_REG_0;
-	else
-		load_reg = insn->src_reg;
-
-	/* check and record load of old value */
-	err = check_reg_arg(env, load_reg, DST_OP);
-	if (err)
-		return err;
-
 	return 0;
 }
 
diff --git a/tools/testing/selftests/bpf/verifier/atomic_bounds.c b/tools/testing/selftests/bpf/verifier/atomic_bounds.c
new file mode 100644
index 000000000000..45030165ed63
--- /dev/null
+++ b/tools/testing/selftests/bpf/verifier/atomic_bounds.c
@@ -0,0 +1,18 @@
+{
+	"BPF_ATOMIC bounds propagation, mem->reg",
+	.insns = {
+		/* a = 0; */
+		BPF_MOV64_IMM(BPF_REG_0, 0),
+		BPF_STX_MEM(BPF_DW, BPF_REG_10, BPF_REG_0, -8),
+		/* b = atomic_fetch_add(&a, 1); */
+		BPF_MOV64_IMM(BPF_REG_1, 1),
+		BPF_ATOMIC_OP(BPF_DW, BPF_ADD | BPF_FETCH, BPF_REG_10, BPF_REG_1, -8),
+		/* Verifier should be able to tell that this infinite loop isn't reachable. */
+		/* if (b) while (true) continue; */
+		BPF_JMP_IMM(BPF_JNE, BPF_REG_1, 0, -1),
+		BPF_EXIT_INSN(),
+	},
+	.result = ACCEPT,
+	.result_unpriv = REJECT,
+	.errstr_unpriv = "back-edge",
+},

base-commit: 232164e041e925a920bfd28e63d5233cfad90b73
-- 
2.30.0.284.gd98b1dd5eaa7-goog

Re: [PATCH bpf-next] bpf: Propagate memory bounds to registers in atomics w/ BPF_FETCH

[Alexei Starovoitov]

On Mon, Jan 18, 2021 at 04:06:13PM +0000, Brendan Jackman wrote:
> When BPF_FETCH is set, atomic instructions load a value from memory
> into a register. The current verifier code first checks via
> check_mem_access whether we can access the memory, and then checks
> via check_reg_arg whether we can write into the register.
> 
> For loads, check_reg_arg has the side-effect of marking the
> register's value as unkonwn, and check_mem_access has the side effect
> of propagating bounds from memory to the register.
> 
> Therefore with the current order, bounds information is thrown away,
> but by simply reversing the order of check_reg_arg
> vs. check_mem_access, we can instead propagate bounds smartly.

I think such improvement makes sense, but please tweak commit log
to mention that check_mem_access() is doing it only for stack pointers.
Since "propagating from memory" is too generic. Most memory
won't have such propagation.

> A simple test is added with an infinite loop that can only be proved
> unreachable if this propagation is present.
> 
> Note that in the test, the memory value has to be written with two
> instructions:
> 
> 		BPF_MOV64_IMM(BPF_REG_0, 0),
> 		BPF_STX_MEM(BPF_DW, BPF_REG_10, BPF_REG_0, -8),
> 
> instead of one:
> 
> 		BPF_ST_MEM(BPF_DW, BPF_REG_10, -8, 0),
> 
> Because BPF_ST_MEM doesn't seem to set the stack slot type to 0 when
> storing an immediate.

This bit is confusing in the commit log. Pls move it into test itself.

> Signed-off-by: Brendan Jackman <jackmanb@google.com>
> ---
>  kernel/bpf/verifier.c                         | 32 +++++++++++--------
>  .../selftests/bpf/verifier/atomic_bounds.c    | 18 +++++++++++
>  2 files changed, 36 insertions(+), 14 deletions(-)
>  create mode 100644 tools/testing/selftests/bpf/verifier/atomic_bounds.c
> 
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 0f82d5d46e2c..0512695c70f4 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -3663,9 +3663,26 @@ static int check_atomic(struct bpf_verifier_env *env, int insn_idx, struct bpf_i
>  		return -EACCES;
>  	}
>  
> +	if (insn->imm & BPF_FETCH) {
> +		if (insn->imm == BPF_CMPXCHG)
> +			load_reg = BPF_REG_0;
> +		else
> +			load_reg = insn->src_reg;
> +
> +		/* check and record load of old value */
> +		err = check_reg_arg(env, load_reg, DST_OP);
> +		if (err)
> +			return err;
> +	} else {
> +		/* This instruction accesses a memory location but doesn't
> +		 * actually load it into a register.
> +		 */
> +		load_reg = -1;
> +	}
> +
>  	/* check whether we can read the memory */
>  	err = check_mem_access(env, insn_idx, insn->dst_reg, insn->off,
> -			       BPF_SIZE(insn->code), BPF_READ, -1, true);
> +			       BPF_SIZE(insn->code), BPF_READ, load_reg, true);
>  	if (err)
>  		return err;
>  
> @@ -3675,19 +3692,6 @@ static int check_atomic(struct bpf_verifier_env *env, int insn_idx, struct bpf_i
>  	if (err)
>  		return err;
>  
> -	if (!(insn->imm & BPF_FETCH))
> -		return 0;
> -
> -	if (insn->imm == BPF_CMPXCHG)
> -		load_reg = BPF_REG_0;
> -	else
> -		load_reg = insn->src_reg;
> -
> -	/* check and record load of old value */
> -	err = check_reg_arg(env, load_reg, DST_OP);
> -	if (err)
> -		return err;
> -
>  	return 0;
>  }
>  
> diff --git a/tools/testing/selftests/bpf/verifier/atomic_bounds.c b/tools/testing/selftests/bpf/verifier/atomic_bounds.c
> new file mode 100644
> index 000000000000..45030165ed63
> --- /dev/null
> +++ b/tools/testing/selftests/bpf/verifier/atomic_bounds.c
> @@ -0,0 +1,18 @@
> +{
> +	"BPF_ATOMIC bounds propagation, mem->reg",
> +	.insns = {
> +		/* a = 0; */
> +		BPF_MOV64_IMM(BPF_REG_0, 0),
> +		BPF_STX_MEM(BPF_DW, BPF_REG_10, BPF_REG_0, -8),
> +		/* b = atomic_fetch_add(&a, 1); */
> +		BPF_MOV64_IMM(BPF_REG_1, 1),
> +		BPF_ATOMIC_OP(BPF_DW, BPF_ADD | BPF_FETCH, BPF_REG_10, BPF_REG_1, -8),
> +		/* Verifier should be able to tell that this infinite loop isn't reachable. */
> +		/* if (b) while (true) continue; */
> +		BPF_JMP_IMM(BPF_JNE, BPF_REG_1, 0, -1),
> +		BPF_EXIT_INSN(),

I think it's a bit unrealistic to use atomic_add to increment induction variable,
but I don't mind, since the verifier side is simple.
Could you add a C based test as well?