[PATCH v2 0/3] Fix truncation bug in coerce_reg_to_size_sx and extend selftests.

[PATCH v2 0/3] Fix truncation bug in coerce_reg_to_size_sx and extend selftests.

[Dimitar Kanaliev]

This patch series addresses a truncation bug in the eBPF verifier function
coerce_reg_to_size_sx(). The issue was caused by the incorrect ordering
of assignments between 32-bit and 64-bit min/max values, leading to
improper truncation when updating the register state. This issue has been
reported previously by Zac Ecob[1] , but was not followed up on.

The first patch fixes the assignment order in coerce_reg_to_size_sx()
to ensure correct truncation. The subsequent patches add selftests for
coerce_{reg,subreg}_to_size_sx.

Changelog:
	v1 -> v2:
	 - Moved selftests inside the conditional check for cpuv4

[1] (https://lore.kernel.org/bpf/h3qKLDEO6m9nhif0eAQX4fVrqdO0D_OPb0y5HfMK9jBePEKK33wQ3K-bqSVnr0hiZdFZtSJOsbNkcEQGpv_yJk61PAAiO8fUkgMRSO-lB50=@protonmail.com/)

Dimitar Kanaliev (3):
  bpf: Fix truncation bug in coerce_reg_to_size_sx()
  selftests/bpf: Add test for truncation after sign extension in
    coerce_reg_to_size_sx()
  selftests/bpf: Add test for sign extension in
    coerce_subreg_to_size_sx()

 kernel/bpf/verifier.c                         |  8 ++--
 .../selftests/bpf/progs/verifier_movsx.c      | 40 +++++++++++++++++++
 2 files changed, 44 insertions(+), 4 deletions(-)

-- 
2.43.0

[PATCH v2 1/3] bpf: Fix truncation bug in coerce_reg_to_size_sx()

[Dimitar Kanaliev]

coerce_reg_to_size_sx() updates the register state after a sign-extension
operation. However, there's a bug in the assignment order of the unsigned
min/max values, leading to incorrect truncation:

  0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
  1: (57) r0 &= 1                       ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
  2: (07) r0 += 254                     ; R0_w=scalar(smin=umin=smin32=umin32=254,smax=umax=smax32=umax32=255,var_off=(0xfe; 0x1))
  3: (bf) r0 = (s8)r0                   ; R0_w=scalar(smin=smin32=-2,smax=smax32=-1,umin=umin32=0xfffffffe,umax=0xffffffff,var_off=(0xfffffffffffffffe; 0x1))

In the current implementation, the unsigned 32-bit min/max values
(u32_min_value and u32_max_value) are assigned directly from the 64-bit
signed min/max values (s64_min and s64_max):

  reg->umin_value = reg->u32_min_value = s64_min;
  reg->umax_value = reg->u32_max_value = s64_max;

Due to the chain assigmnent, this is equivalent to:

  reg->u32_min_value = s64_min;  // Unintended truncation
  reg->umin_value = reg->u32_min_value;
  reg->u32_max_value = s64_max;  // Unintended truncation
  reg->umax_value = reg->u32_max_value;

Fixes: 1f9a1ea821ff ("bpf: Support new sign-extension load insns")
Reported-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Reported-by: Zac Ecob <zacecob@protonmail.com>
Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>
---
 kernel/bpf/verifier.c | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 7d9b38ffd220..70a0cf0f1569 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -6333,10 +6333,10 @@ static void coerce_reg_to_size_sx(struct bpf_reg_state *reg, int size)
 
 	/* both of s64_max/s64_min positive or negative */
 	if ((s64_max >= 0) == (s64_min >= 0)) {
-		reg->smin_value = reg->s32_min_value = s64_min;
-		reg->smax_value = reg->s32_max_value = s64_max;
-		reg->umin_value = reg->u32_min_value = s64_min;
-		reg->umax_value = reg->u32_max_value = s64_max;
+		reg->s32_min_value = reg->smin_value = s64_min;
+		reg->s32_max_value = reg->smax_value = s64_max;
+		reg->u32_min_value = reg->umin_value = s64_min;
+		reg->u32_max_value = reg->umax_value = s64_max;
 		reg->var_off = tnum_range(s64_min, s64_max);
 		return;
 	}
-- 
2.43.0

[PATCH v2 2/3] selftests/bpf: Add test for truncation after sign extension in coerce_reg_to_size_sx()

[Dimitar Kanaliev]

Add test that checks whether unsigned ranges deduced by the verifier for
sign extension instruction is correct. Without previous patch that
fixes truncation in coerce_reg_to_size_sx() this test fails.

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>
---
 .../selftests/bpf/progs/verifier_movsx.c      | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_movsx.c b/tools/testing/selftests/bpf/progs/verifier_movsx.c
index 028ec855587b..0cb879c609c5 100644
--- a/tools/testing/selftests/bpf/progs/verifier_movsx.c
+++ b/tools/testing/selftests/bpf/progs/verifier_movsx.c
@@ -287,6 +287,26 @@ l0_%=:							\
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("MOV64SX, S8, unsigned range_check")
+__success __retval(0)
+__naked void mov64sx_s8_range_check(void)
+{
+	asm volatile ("					\
+	call %[bpf_get_prandom_u32];			\
+	r0 &= 0x1;					\
+	r0 += 0xfe;					\
+	r0 = (s8)r0;					\
+	if r0 < 0xfffffffffffffffe goto label_%=;	\
+	r0 = 0;						\
+	exit;						\
+label_%=:						\
+	exit;						\
+"	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 #else
 
 SEC("socket")
-- 
2.43.0

[PATCH v2 3/3] selftests/bpf: Add test for sign extension in coerce_subreg_to_size_sx()

[Dimitar Kanaliev]

Add a test for unsigned ranges after signed extension instruction. This
case isn't currently covered by existing tests in verifier_movsx.c.

Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>
---
 .../selftests/bpf/progs/verifier_movsx.c      | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_movsx.c b/tools/testing/selftests/bpf/progs/verifier_movsx.c
index 0cb879c609c5..994bbc346d25 100644
--- a/tools/testing/selftests/bpf/progs/verifier_movsx.c
+++ b/tools/testing/selftests/bpf/progs/verifier_movsx.c
@@ -307,6 +307,26 @@ label_%=:						\
 	: __clobber_all);
 }
 
+SEC("socket")
+__description("MOV32SX, S8, unsigned range_check")
+__success __retval(0)
+__naked void mov32sx_s8_range_check(void)
+{
+	asm volatile ("                                 \
+	call %[bpf_get_prandom_u32];                    \
+	w0 &= 0x1;                                      \
+	w0 += 0xfe;                                     \
+	w0 = (s8)w0;                                    \
+	if w0 < 0xfffffffe goto label_%=;               \
+	r0 = 0;                                         \
+	exit;                                           \
+label_%=: 	                                        \
+	exit;                                           \
+	"      :
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 #else
 
 SEC("socket")
-- 
2.43.0

Re: [PATCH v2 1/3] bpf: Fix truncation bug in coerce_reg_to_size_sx()

[Yonghong Song]

On 10/14/24 5:11 AM, Dimitar Kanaliev wrote:
> coerce_reg_to_size_sx() updates the register state after a sign-extension
> operation. However, there's a bug in the assignment order of the unsigned
> min/max values, leading to incorrect truncation:
>
>    0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
>    1: (57) r0 &= 1                       ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
>    2: (07) r0 += 254                     ; R0_w=scalar(smin=umin=smin32=umin32=254,smax=umax=smax32=umax32=255,var_off=(0xfe; 0x1))
>    3: (bf) r0 = (s8)r0                   ; R0_w=scalar(smin=smin32=-2,smax=smax32=-1,umin=umin32=0xfffffffe,umax=0xffffffff,var_off=(0xfffffffffffffffe; 0x1))
>
> In the current implementation, the unsigned 32-bit min/max values
> (u32_min_value and u32_max_value) are assigned directly from the 64-bit
> signed min/max values (s64_min and s64_max):
>
>    reg->umin_value = reg->u32_min_value = s64_min;
>    reg->umax_value = reg->u32_max_value = s64_max;
>
> Due to the chain assigmnent, this is equivalent to:
>
>    reg->u32_min_value = s64_min;  // Unintended truncation
>    reg->umin_value = reg->u32_min_value;
>    reg->u32_max_value = s64_max;  // Unintended truncation
>    reg->umax_value = reg->u32_max_value;
>
> Fixes: 1f9a1ea821ff ("bpf: Support new sign-extension load insns")
> Reported-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Reported-by: Zac Ecob <zacecob@protonmail.com>
> Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>

Thanks for the fix!

Acked-by: Yonghong Song <yonghong.song@linux.dev>

Re: [PATCH v2 2/3] selftests/bpf: Add test for truncation after sign extension in coerce_reg_to_size_sx()

[Yonghong Song]

On 10/14/24 5:11 AM, Dimitar Kanaliev wrote:
> Add test that checks whether unsigned ranges deduced by the verifier for
> sign extension instruction is correct. Without previous patch that
> fixes truncation in coerce_reg_to_size_sx() this test fails.
>
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>

Acked-by: Yonghong Song <yonghong.song@linux.dev>

Re: [PATCH v2 3/3] selftests/bpf: Add test for sign extension in coerce_subreg_to_size_sx()

[Yonghong Song]

On 10/14/24 5:11 AM, Dimitar Kanaliev wrote:
> Add a test for unsigned ranges after signed extension instruction. This
> case isn't currently covered by existing tests in verifier_movsx.c.
>
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>

Acked-by: Yonghong Song <yonghong.song@linux.dev>

Re: [PATCH v2 1/3] bpf: Fix truncation bug in coerce_reg_to_size_sx()

[Shung-Hsi Yu]

On Mon, Oct 14, 2024 at 03:11:53PM GMT, Dimitar Kanaliev wrote:
> coerce_reg_to_size_sx() updates the register state after a sign-extension
> operation. However, there's a bug in the assignment order of the unsigned
> min/max values, leading to incorrect truncation:
> 
>   0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
>   1: (57) r0 &= 1                       ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
>   2: (07) r0 += 254                     ; R0_w=scalar(smin=umin=smin32=umin32=254,smax=umax=smax32=umax32=255,var_off=(0xfe; 0x1))
>   3: (bf) r0 = (s8)r0                   ; R0_w=scalar(smin=smin32=-2,smax=smax32=-1,umin=umin32=0xfffffffe,umax=0xffffffff,var_off=(0xfffffffffffffffe; 0x1))
> 
> In the current implementation, the unsigned 32-bit min/max values
> (u32_min_value and u32_max_value) are assigned directly from the 64-bit
> signed min/max values (s64_min and s64_max):
> 
>   reg->umin_value = reg->u32_min_value = s64_min;
>   reg->umax_value = reg->u32_max_value = s64_max;
> 
> Due to the chain assigmnent, this is equivalent to:
> 
>   reg->u32_min_value = s64_min;  // Unintended truncation
>   reg->umin_value = reg->u32_min_value;
>   reg->u32_max_value = s64_max;  // Unintended truncation
>   reg->umax_value = reg->u32_max_value;

Nit: while I initially suggested the above fragment to Dimitar to use in
commit message, perhaps saying that "reg->u32_min_value = s64_min" is an
unintended truncation is not entirely correct; we do want truncation in
"reg->u32_max_value = (u32)s64_max" to happen, just not
"reg->umax_value = (u32)s64_max". Hopefully the maintainer knows a more
elegant way to put it.

Other than that,

Reviewed-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>

> Fixes: 1f9a1ea821ff ("bpf: Support new sign-extension load insns")
> Reported-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Reported-by: Zac Ecob <zacecob@protonmail.com>
> Signed-off-by: Dimitar Kanaliev <dimitar.kanaliev@siteground.com>
...

Re: [PATCH v2 1/3] bpf: Fix truncation bug in coerce_reg_to_size_sx()

[Shung-Hsi Yu]

[-- Attachment #1: Type: text/plain, Size: 4915 bytes --]

On Mon, Oct 14, 2024 at 03:11:53PM GMT, Dimitar Kanaliev wrote:
> coerce_reg_to_size_sx() updates the register state after a sign-extension
> operation. However, there's a bug in the assignment order of the unsigned
> min/max values, leading to incorrect truncation:
> 
>   0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
>   1: (57) r0 &= 1                       ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1))
>   2: (07) r0 += 254                     ; R0_w=scalar(smin=umin=smin32=umin32=254,smax=umax=smax32=umax32=255,var_off=(0xfe; 0x1))
>   3: (bf) r0 = (s8)r0                   ; R0_w=scalar(smin=smin32=-2,smax=smax32=-1,umin=umin32=0xfffffffe,umax=0xffffffff,var_off=(0xfffffffffffffffe; 0x1))
> 
> In the current implementation, the unsigned 32-bit min/max values
> (u32_min_value and u32_max_value) are assigned directly from the 64-bit
> signed min/max values (s64_min and s64_max):
> 
>   reg->umin_value = reg->u32_min_value = s64_min;
>   reg->umax_value = reg->u32_max_value = s64_max;
> 
> Due to the chain assigmnent, this is equivalent to:
> 
>   reg->u32_min_value = s64_min;  // Unintended truncation
>   reg->umin_value = reg->u32_min_value;
>   reg->u32_max_value = s64_max;  // Unintended truncation
>   reg->umax_value = reg->u32_max_value;
> 
> Fixes: 1f9a1ea821ff ("bpf: Support new sign-extension load insns")
> Reported-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Reported-by: Zac Ecob <zacecob@protonmail.com>

FWIW sharing the CMBC checking .c file that found this bug 2 weeks back
(though Zac already discovered and debugged this back in July, which I
realized quite late). The command I used is simply

	cbmc --trace $ATTACHED_C_FILE

Which rougly reporting that the assertation in following piece of
(pseudo) code is failing:

	u64 x; /* assume reg.umin <= x <= reg.umax initially */
	struct bpf_reg_state reg, new_reg;
	u64 new_x;
	
	coerce_reg_to_size_sx(&new_reg, size);
	assert(new_reg.umin_value <= new_x);
	assert(new_x <= new_reg.umax_value);

It then takes some effort to dig through the CBMC traces backwards to
find the relevant parts. First finding where umin and umax was set to
locate the problematic code (CBMC points to line 140 and 141 in the
attached file):

	State 178 file tmp/coerce_reg_to_size_sx-verify.c function coerce_reg_to_size_sx line 140 thread 0
	----------------------------------------------------
	new_reg.umin_value=4294967294ul (00000000 00000000 00000000 00000000 11111111 11111111 11111111 11111110)
	...
	State 182 file tmp/coerce_reg_to_size_sx-verify.c function coerce_reg_to_size_sx line 141 thread 0
	----------------------------------------------------
	new_reg.umax_value=4294967295ul (00000000 00000000 00000000 00000000 11111111 11111111 11111111 11111111)

Then get the used inital input by looking further back (note: I
explicitly asked CBMC to find a case where coerce_reg_to_size_sx()
doesn't work where var_off.mask==1 to make things simpler):

	State 30 file tmp/coerce_reg_to_size_sx-verify.c function verify_coerce_reg_to_size_sx line 162 thread 0
	----------------------------------------------------
	reg.var_off.value=254ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 11111110)
	
	State 36 file tmp/coerce_reg_to_size_sx-verify.c function verify_coerce_reg_to_size_sx line 163 thread 0
	----------------------------------------------------
	reg.var_off.mask=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
	
	State 42 file tmp/coerce_reg_to_size_sx-verify.c function verify_coerce_reg_to_size_sx line 164 thread 0
	----------------------------------------------------
	reg.smin_value=254l (00000000 00000000 00000000 00000000 00000000 00000000 00000000 11111110)
	
	State 48 file tmp/coerce_reg_to_size_sx-verify.c function verify_coerce_reg_to_size_sx line 165 thread 0
	----------------------------------------------------
	reg.smax_value=255l (00000000 00000000 00000000 00000000 00000000 00000000 00000000 11111111)
	
	State 54 file tmp/coerce_reg_to_size_sx-verify.c function verify_coerce_reg_to_size_sx line 166 thread 0
	----------------------------------------------------
	reg.umin_value=254ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 11111110)
	
	State 60 file tmp/coerce_reg_to_size_sx-verify.c function verify_coerce_reg_to_size_sx line 167 thread 0
	----------------------------------------------------
	reg.umax_value=255ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 11111111)
	...

Which summarizes down to the input bpf_reg_state being

	struct bpf_reg_state reg = {
		.var_off = { mask=0x1, value=0xfe },
		.smin_value = 254,
		.smax_value = 255,
		.umin_value = 254,
		.umax_value = 255,
		/* 32-bit ranges aren't used as input and I couldn't get them
		 * generate right, so omitted here.
		 */
		...		 
	}

And from there things were largely straightforward to debug.

[snip]

[-- Attachment #2: Type: text/plain, Size: 8150 bytes --]

#include <stdint.h>
#include <limits.h>
#include <stdbool.h>
#include <assert.h>

// Define Linux kernel types
typedef uint64_t u64;
typedef int64_t s64;
typedef uint32_t u32;
typedef int32_t s32;
typedef uint8_t u8;
typedef int8_t s8;
typedef uint16_t u16;
typedef int16_t s16;

// Define limits
#define S8_MIN  INT8_MIN
#define S8_MAX  INT8_MAX
#define S16_MIN INT16_MIN
#define S16_MAX INT16_MAX
#define S32_MIN INT32_MIN
#define S32_MAX INT32_MAX
#define U32_MAX UINT32_MAX
#define S64_MIN INT64_MIN
#define S64_MAX INT64_MAX
#define U64_MAX UINT64_MAX

struct tnum {
	u64 value;
	u64 mask;
};

// Simplified version of bpf_reg_state with only field needed by
// coerce_reg_to_size_sx
struct bpf_reg_state {
	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;
};

// Global variable for unknown tnum
const struct tnum tnum_unknown = {.value = 0, .mask = U64_MAX};

// Helper functions
bool tnum_is_const(struct tnum t) {
	return t.mask == 0;
}

struct tnum tnum_range(u64 min, u64 max) {
	struct tnum t;
	u64 chi = min ^ max;
	u64 bits = 64 - __builtin_clzll(chi);
	u64 mask = (1ULL << bits) - 1;

	if (bits > 63)
		return tnum_unknown;

	t.value = min & ~mask;
	t.mask = mask;
	return t;
}
bool tnum_contains(struct tnum t, u64 v) {
	return (v & ~t.mask) == t.value;
}

static void set_sext64_default_val(struct bpf_reg_state *reg, int size)
{
	if (size == 1) {
		reg->smin_value = reg->s32_min_value = S8_MIN;
		reg->smax_value = reg->s32_max_value = S8_MAX;
	} else if (size == 2) {
		reg->smin_value = reg->s32_min_value = S16_MIN;
		reg->smax_value = reg->s32_max_value = S16_MAX;
	} else {
		/* size == 4 */
		reg->smin_value = reg->s32_min_value = S32_MIN;
		reg->smax_value = reg->s32_max_value = S32_MAX;
	}
	reg->umin_value = reg->u32_min_value = 0;
	reg->umax_value = U64_MAX;
	reg->u32_max_value = U32_MAX;
	reg->var_off = tnum_unknown;
}

static void coerce_reg_to_size_sx(struct bpf_reg_state *reg, int size)
{
	s64 init_s64_max, init_s64_min, s64_max, s64_min, u64_cval;
	u64 top_smax_value, top_smin_value;
	u64 num_bits = size * 8;

	if (tnum_is_const(reg->var_off)) {
		u64_cval = reg->var_off.value;
		if (size == 1)
			reg->var_off = tnum_range((s8)u64_cval, (s8)u64_cval);
		else if (size == 2)
			reg->var_off = tnum_range((s16)u64_cval, (s16)u64_cval);
		else
			/* size == 4 */
			reg->var_off = tnum_range((s32)u64_cval, (s32)u64_cval);

		u64_cval = reg->var_off.value;
		reg->smax_value = reg->smin_value = u64_cval;
		reg->umax_value = reg->umin_value = u64_cval;
		reg->s32_max_value = reg->s32_min_value = u64_cval;
		reg->u32_max_value = reg->u32_min_value = u64_cval;
		return;
	}

	top_smax_value = ((u64)reg->smax_value >> num_bits) << num_bits;
	top_smin_value = ((u64)reg->smin_value >> num_bits) << num_bits;

	if (top_smax_value != top_smin_value)
		goto out;

	/* find the s64_min and s64_min after sign extension */
	if (size == 1) {
		init_s64_max = (s8)reg->smax_value;
		init_s64_min = (s8)reg->smin_value;
	} else if (size == 2) {
		init_s64_max = (s16)reg->smax_value;
		init_s64_min = (s16)reg->smin_value;
	} else {
		init_s64_max = (s32)reg->smax_value;
		init_s64_min = (s32)reg->smin_value;
	}

	s64_max = (init_s64_max > init_s64_min) ? init_s64_max : init_s64_min;
	s64_min = (init_s64_max < init_s64_min) ? init_s64_max : init_s64_min;

	/* both of s64_max/s64_min positive or negative */
	if ((s64_max >= 0) == (s64_min >= 0)) {
		reg->smin_value = reg->s32_min_value = s64_min;
		reg->smax_value = reg->s32_max_value = s64_max;
		reg->umin_value = reg->u32_min_value = s64_min;
		reg->umax_value = reg->u32_max_value = s64_max;
		reg->var_off = tnum_range(s64_min, s64_max);
		return;
	}

out:
	set_sext64_default_val(reg, size);
}

void verify_coerce_reg_to_size_sx()
{
	struct bpf_reg_state reg, new_reg;
	u64 x, new_x;
	int size;

	// Assume valid argument given to coerce_reg_to_size_sx()
	size = __CPROVER_int_input();
	__CPROVER_assume(size == 1 || size == 2 || size == 4);

	// Use CBMC's built-in nondeterministic functions to generate
	// struct bpf_reg_state that we're using as input
	reg.var_off.value = __CPROVER_unsigned_long_long_input();
	reg.var_off.mask = __CPROVER_unsigned_long_long_input();
	reg.smin_value = __CPROVER_long_long_input();
	reg.smax_value = __CPROVER_long_long_input();
	reg.umin_value = __CPROVER_unsigned_long_long_input();
	reg.umax_value = __CPROVER_unsigned_long_long_input();
	reg.s32_min_value = __CPROVER_int_input();
	reg.s32_max_value = __CPROVER_int_input();
	reg.u32_min_value = __CPROVER_unsigned_int_input();
	reg.u32_max_value = __CPROVER_unsigned_int_input();

	// Below are some assumption about how bounds in bpf_reg_state relates
	// for a reasonable and conherent bound in bpf_reg_state, however I
	// don't have any prove that this is a valid description of how bounds
	// in bpf_reg_state related, anyhow:

	// Assumptions about var_off and min/max values
	__CPROVER_assume(reg.var_off.value <= reg.umin_value);
	__CPROVER_assume(reg.var_off.value | reg.var_off.mask >= reg.umax_value);
	// Ensure umin_value <= umax_value
	__CPROVER_assume(reg.umin_value <= reg.umax_value);
	// Ensure smin_value <= smax_value
	__CPROVER_assume(reg.smin_value <= reg.smax_value);
	// Ensure u32_min_value <= u32_max_value
	__CPROVER_assume(reg.u32_min_value <= reg.u32_max_value);
	// Ensure s32_min_value <= s32_max_value
	__CPROVER_assume(reg.s32_min_value <= reg.s32_max_value);
	// Ensure 64-bit bounds are consistent with 32-bit bounds
	__CPROVER_assume(reg.umin_value <= (u64)reg.u32_max_value);
	__CPROVER_assume(reg.umax_value >= (u64)reg.u32_min_value);
	__CPROVER_assume((s64)reg.smin_value <= (s64)reg.s32_max_value);
	__CPROVER_assume((s64)reg.smax_value >= (s64)reg.s32_min_value);
	// Bound-crossing situations
	if (reg.var_off.value <= (u64)S64_MAX && (u64)S64_MIN <= (reg.var_off.value | reg.var_off.mask)) {
		__CPROVER_assume(reg.smin_value == S64_MIN && reg.smax_value == S64_MAX);
	} else if (reg.smin_value < 0 && reg.smax_value >= 0) {
		__CPROVER_assume(reg.var_off.value == 0 && reg.var_off.mask == U64_MAX);
		__CPROVER_assume(reg.umin_value == 0 && reg.umax_value == U64_MAX);
	} else {
		__CPROVER_assume(reg.umin_value == (u64)reg.smin_value && reg.umax_value == (u64)reg.smax_value);
	}
	// Probably need more relation between 32-bit range bounds...


	// Assuming we have some x
	x = __CPROVER_unsigned_long_long_input();
	// Mimick the sign-extension ourself
	new_x = (s64)((s64)x << (64 - size*8)) >> (64 - size*8);
	// Now say x could be ANY value that's bpf_reg_state represents
	__CPROVER_assume((reg.var_off.value & reg.var_off.mask) == 0); // tnum wellformedness
	__CPROVER_assume(tnum_contains(reg.var_off, x));
	__CPROVER_assume(reg.umin_value <= x && x <= reg.umax_value);
	__CPROVER_assume((s64)reg.smin_value <= (s64)x && (s64)x <= (s64)reg.smax_value);
	__CPROVER_assume((u32)reg.u32_min_value <= (u32)x && (u32)x <= (u32)reg.u32_max_value);
	__CPROVER_assume((s32)reg.s32_min_value <= (s32)x && (s32)x <= (s32)reg.s32_max_value);

	/* Since we know this will fail, we can have some additional contraints
	 * to "shrink" the input to something easier to consume for our human
	 * mind.
	 */
	__CPROVER_assume(x == 255);
	__CPROVER_assume(size == 1);
	__CPROVER_assume(reg.var_off.mask == 1);
	__CPROVER_assume(reg.umax_value - reg.umin_value == 1);
	__CPROVER_assume(reg.smax_value - reg.smin_value == 1);

	// Runs coerce_reg_to_size_sx()
	new_reg = reg;
	coerce_reg_to_size_sx(&new_reg, size);

	// Now ask CBMC to check that the sign-extended value of x is still
	// represented by bpf_reg_state after coerce_reg_to_size_sx()
	assert(new_reg.umin_value <= new_x && new_x <= new_reg.umax_value);
	assert(tnum_contains(new_reg.var_off, new_x));
	assert((s64)new_reg.smin_value <= (s64)new_x && (s64)new_x <= (s64)new_reg.smax_value);
	assert((u32)new_reg.u32_min_value <= (u32)new_x && (u32)new_x <= (u32)new_reg.u32_max_value);
	assert((s32)new_reg.s32_min_value <= (s32)new_x && (s32)new_x <= (s32)new_reg.s32_max_value);
}

int main()
{
	verify_coerce_reg_to_size_sx();
	return 0;
}

Re: [PATCH v2 0/3] Fix truncation bug in coerce_reg_to_size_sx and extend selftests.

[patchwork-bot+netdevbpf]

Hello:

This series was applied to bpf/bpf.git (master)
by Alexei Starovoitov <ast@kernel.org>:

On Mon, 14 Oct 2024 15:11:52 +0300 you wrote:
> This patch series addresses a truncation bug in the eBPF verifier function
> coerce_reg_to_size_sx(). The issue was caused by the incorrect ordering
> of assignments between 32-bit and 64-bit min/max values, leading to
> improper truncation when updating the register state. This issue has been
> reported previously by Zac Ecob[1] , but was not followed up on.
> 
> The first patch fixes the assignment order in coerce_reg_to_size_sx()
> to ensure correct truncation. The subsequent patches add selftests for
> coerce_{reg,subreg}_to_size_sx.
> 
> [...]

Here is the summary with links:
  - [v2,1/3] bpf: Fix truncation bug in coerce_reg_to_size_sx()
    https://git.kernel.org/bpf/bpf/c/ae67b9fb8c4e
  - [v2,2/3] selftests/bpf: Add test for truncation after sign extension in coerce_reg_to_size_sx()
    https://git.kernel.org/bpf/bpf/c/61f506eacc77
  - [v2,3/3] selftests/bpf: Add test for sign extension in coerce_subreg_to_size_sx()
    https://git.kernel.org/bpf/bpf/c/35ccd576a23c

You are awesome, thank you!
-- 
Deet-doot-dot, I am a bot.
https://korg.docs.kernel.org/patchwork/pwbot.html