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@xxxxxxxx>
> Reported-by: Zac Ecob <zacecob@xxxxxxxxxxxxxx>
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]
#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;
}
