bpf: incorrect value spill in check_stack_write_fixed_off()

bpf: incorrect value spill in check_stack_write_fixed_off()

[Hao Sun]

Hi,

In check_stack_write_fixed_off(), the verifier creates a fake reg to store the
imm in a BPF_ST_MEM:
...
else if (!reg && !(off % BPF_REG_SIZE) && is_bpf_st_mem(insn) &&
insn->imm != 0 && env->bpf_capable) {
        struct bpf_reg_state fake_reg = {};

        __mark_reg_known(&fake_reg, (u32)insn->imm);
        fake_reg.type = SCALAR_VALUE;
        save_register_state(state, spi, &fake_reg, size);

Here, insn->imm is cast to u32, and used to mark fake_reg, which is incorrect
and may lose sign information. Consider the following program:

r2 = r10
*(u64*)(r2 -40) = -44
r0 = *(u64*)(r2 - 40)
if r0 s<= 0xa goto +2
r0 = 0
exit
r0  = 1
exit

The verifier gives the following log:

-------- Verifier Log --------
func#0 @0
0: R1=ctx(off=0,imm=0) R10=fp0
0: (bf) r2 = r10                      ; R2_w=fp0 R10=fp0
1: (7a) *(u64 *)(r2 -40) = -44        ; R2_w=fp0 fp-40_w=4294967252
2: (79) r0 = *(u64 *)(r2 -40)         ; R0_w=4294967252 R2_w=fp0
fp-40_w=4294967252
3: (c5) if r0 s< 0xa goto pc+2
mark_precise: frame0: last_idx 3 first_idx 0 subseq_idx -1
mark_precise: frame0: regs=r0 stack= before 2: (79) r0 = *(u64 *)(r2 -40)
3: R0_w=4294967252
4: (b7) r0 = 1                        ; R0_w=1
5: (95) exit
verification time 7971 usec
stack depth 40
processed 6 insns (limit 1000000) max_states_per_insn 0 total_states 0
peak_states 0 mark_read 0

Here, the verifier incorrectly thinks R0 is 0xffffffd4, which should
be 0xffffffffffffffd4,
due to the u32 cast in check_stack_write_fixed_off(). This makes the verifier
collect incorrect reg scalar range.

Since insn->imm is i32, we should cast it to the signed integer with
correct size
according to BPF_MEM, then promoting the imm to u64 to mark fake reg as
known, right?

Best
Hao

Re: bpf: incorrect value spill in check_stack_write_fixed_off()

[Hao Sun]

On Wed, Oct 25, 2023 at 11:16 AM Hao Sun <sunhao.th@gmail.com> wrote:
>
> Hi,
>
> In check_stack_write_fixed_off(), the verifier creates a fake reg to store the
> imm in a BPF_ST_MEM:
> ...
> else if (!reg && !(off % BPF_REG_SIZE) && is_bpf_st_mem(insn) &&
> insn->imm != 0 && env->bpf_capable) {
>         struct bpf_reg_state fake_reg = {};
>
>         __mark_reg_known(&fake_reg, (u32)insn->imm);
>         fake_reg.type = SCALAR_VALUE;
>         save_register_state(state, spi, &fake_reg, size);
>
> Here, insn->imm is cast to u32, and used to mark fake_reg, which is incorrect
> and may lose sign information. Consider the following program:
>
> r2 = r10
> *(u64*)(r2 -40) = -44
> r0 = *(u64*)(r2 - 40)
> if r0 s<= 0xa goto +2
> r0 = 0
> exit
> r0  = 1
> exit
>

Sorry, the program should be:

 r2 = r10
 *(u64*)(r2 -40) = -44
 r0 = *(u64*)(r2 - 40)
 if r0 s<= 0xa goto +2
 r0 = 1
 exit
 r0  = 0
 exit

Here is the C macros for the following verifier's log:

BPF_MOV64_REG(BPF_REG_2, BPF_REG_10),
BPF_ST_MEM(BPF_DW, BPF_REG_2, -40, -44),
BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_2, -40),
BPF_JMP_IMM(BPF_JSLT, BPF_REG_0, 0xa, 2),
BPF_MOV64_IMM(BPF_REG_0, 1),
BPF_EXIT_INSN(),
BPF_MOV64_IMM(BPF_REG_0, 0),
BPF_EXIT_INSN()

> The verifier gives the following log:
>
> -------- Verifier Log --------
> func#0 @0
> 0: R1=ctx(off=0,imm=0) R10=fp0
> 0: (bf) r2 = r10                      ; R2_w=fp0 R10=fp0
> 1: (7a) *(u64 *)(r2 -40) = -44        ; R2_w=fp0 fp-40_w=4294967252
> 2: (79) r0 = *(u64 *)(r2 -40)         ; R0_w=4294967252 R2_w=fp0
> fp-40_w=4294967252
> 3: (c5) if r0 s< 0xa goto pc+2
> mark_precise: frame0: last_idx 3 first_idx 0 subseq_idx -1
> mark_precise: frame0: regs=r0 stack= before 2: (79) r0 = *(u64 *)(r2 -40)
> 3: R0_w=4294967252
> 4: (b7) r0 = 1                        ; R0_w=1
> 5: (95) exit
> verification time 7971 usec
> stack depth 40
> processed 6 insns (limit 1000000) max_states_per_insn 0 total_states 0
> peak_states 0 mark_read 0
>
> Here, the verifier incorrectly thinks R0 is 0xffffffd4, which should
> be 0xffffffffffffffd4,
> due to the u32 cast in check_stack_write_fixed_off(). This makes the verifier
> collect incorrect reg scalar range.
>
> Since insn->imm is i32, we should cast it to the signed integer with
> correct size
> according to BPF_MEM, then promoting the imm to u64 to mark fake reg as
> known, right?
>
> Best
> Hao

Re: bpf: incorrect value spill in check_stack_write_fixed_off()

[Eduard Zingerman]

On Wed, 2023-10-25 at 11:16 +0200, Hao Sun wrote:
> Hi,
> 
> In check_stack_write_fixed_off(), the verifier creates a fake reg to store the
> imm in a BPF_ST_MEM:
> ...
> else if (!reg && !(off % BPF_REG_SIZE) && is_bpf_st_mem(insn) &&
> insn->imm != 0 && env->bpf_capable) {
>         struct bpf_reg_state fake_reg = {};
> 
>         __mark_reg_known(&fake_reg, (u32)insn->imm);
>         fake_reg.type = SCALAR_VALUE;
>         save_register_state(state, spi, &fake_reg, size);
> 
> Here, insn->imm is cast to u32, and used to mark fake_reg, which is incorrect
> and may lose sign information.

This bug is on me.
Thank you for reporting it along with the example program.
Looks like the patch below is sufficient to fix the issue.
Have no idea at the moment why I used u32 cast there.
Let me think a bit more about it and I'll submit an official patch.

Thanks,
Eduard

---

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 857d76694517..44af69ce1301 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -4674,7 +4674,7 @@ static int check_stack_write_fixed_off(struct bpf_verifier_env *env,
                   insn->imm != 0 && env->bpf_capable) {
                struct bpf_reg_state fake_reg = {};
 
-               __mark_reg_known(&fake_reg, (u32)insn->imm);
+               __mark_reg_known(&fake_reg, insn->imm);
                fake_reg.type = SCALAR_VALUE;
                save_register_state(state, spi, &fake_reg, size);
        } else if (reg && is_spillable_regtype(reg->type)) {

Re: bpf: incorrect value spill in check_stack_write_fixed_off()

[Eduard Zingerman]

On Wed, 2023-10-25 at 15:14 +0300, Eduard Zingerman wrote:
> On Wed, 2023-10-25 at 11:16 +0200, Hao Sun wrote:
> > Hi,
> > 
> > In check_stack_write_fixed_off(), the verifier creates a fake reg to store the
> > imm in a BPF_ST_MEM:
> > ...
> > else if (!reg && !(off % BPF_REG_SIZE) && is_bpf_st_mem(insn) &&
> > insn->imm != 0 && env->bpf_capable) {
> >         struct bpf_reg_state fake_reg = {};
> > 
> >         __mark_reg_known(&fake_reg, (u32)insn->imm);
> >         fake_reg.type = SCALAR_VALUE;
> >         save_register_state(state, spi, &fake_reg, size);
> > 
> > Here, insn->imm is cast to u32, and used to mark fake_reg, which is incorrect
> > and may lose sign information.
> 
> This bug is on me.
> Thank you for reporting it along with the example program.
> Looks like the patch below is sufficient to fix the issue.
> Have no idea at the moment why I used u32 cast there.
> Let me think a bit more about it and I'll submit an official patch.

Yeap, I see no drawbacks in that patch, imm field is declared as s32,
so it would be correctly sign extended by compiler before cast to u64,
so there is no need for additional casts.
It would be wrong if I submit the fix, because you've done all the work.
Here is a refined test-case to be placed in verifier/bpf_st_mem.c
(be careful with \t, test_verifier uses those as glob marks inside errstr).

{
	"BPF_ST_MEM stack imm sign",
	/* Check if verifier correctly reasons about sign of an
	 * immediate spilled to stack by BPF_ST instruction.
	 *
	 *   fp[-8] = -44;
	 *   r0 = fp[-8];
	 *   if r0 s< 0 goto ret0;
	 *   r0 = -1;
	 *   exit;
	 * ret0:
	 *   r0 = 0;
	 *   exit;
	 */
	.insns = {
	BPF_ST_MEM(BPF_DW, BPF_REG_10, -8, -44),
	BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_10, -8),
	BPF_JMP_IMM(BPF_JSLT, BPF_REG_0, 0, 2),
	BPF_MOV64_IMM(BPF_REG_0, -1),
	BPF_EXIT_INSN(),
	BPF_MOV64_IMM(BPF_REG_0, 0),
	BPF_EXIT_INSN(),
	},
	/* Use prog type that requires return value in range [0, 1] */
	.prog_type = BPF_PROG_TYPE_SK_LOOKUP,
	.expected_attach_type = BPF_SK_LOOKUP,
	.result = VERBOSE_ACCEPT,
	.runs = -1,
	.errstr = "0: (7a) *(u64 *)(r10 -8) = -44        ; R10=fp0 fp-8_w=-44\
	2: (c5) if r0 s< 0x0 goto pc+2\
	2: R0_w=-44",
},

Re: bpf: incorrect value spill in check_stack_write_fixed_off()

[Hao Sun]

On Wed, Oct 25, 2023 at 2:48 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Wed, 2023-10-25 at 15:14 +0300, Eduard Zingerman wrote:
> > On Wed, 2023-10-25 at 11:16 +0200, Hao Sun wrote:
> > > Hi,
> > >
> > > In check_stack_write_fixed_off(), the verifier creates a fake reg to store the
> > > imm in a BPF_ST_MEM:
> > > ...
> > > else if (!reg && !(off % BPF_REG_SIZE) && is_bpf_st_mem(insn) &&
> > > insn->imm != 0 && env->bpf_capable) {
> > >         struct bpf_reg_state fake_reg = {};
> > >
> > >         __mark_reg_known(&fake_reg, (u32)insn->imm);
> > >         fake_reg.type = SCALAR_VALUE;
> > >         save_register_state(state, spi, &fake_reg, size);
> > >
> > > Here, insn->imm is cast to u32, and used to mark fake_reg, which is incorrect
> > > and may lose sign information.
> >
> > This bug is on me.
> > Thank you for reporting it along with the example program.
> > Looks like the patch below is sufficient to fix the issue.
> > Have no idea at the moment why I used u32 cast there.
> > Let me think a bit more about it and I'll submit an official patch.
>
> Yeap, I see no drawbacks in that patch, imm field is declared as s32,
> so it would be correctly sign extended by compiler before cast to u64,
> so there is no need for additional casts.
> It would be wrong if I submit the fix, because you've done all the work.

Done. Besides, users or binaries with CAP_BPF can exploit this bug.

> Here is a refined test-case to be placed in verifier/bpf_st_mem.c
> (be careful with \t, test_verifier uses those as glob marks inside errstr).
>
> {
>         "BPF_ST_MEM stack imm sign",
>         /* Check if verifier correctly reasons about sign of an
>          * immediate spilled to stack by BPF_ST instruction.
>          *
>          *   fp[-8] = -44;
>          *   r0 = fp[-8];
>          *   if r0 s< 0 goto ret0;
>          *   r0 = -1;
>          *   exit;
>          * ret0:
>          *   r0 = 0;
>          *   exit;
>          */
>         .insns = {
>         BPF_ST_MEM(BPF_DW, BPF_REG_10, -8, -44),
>         BPF_LDX_MEM(BPF_DW, BPF_REG_0, BPF_REG_10, -8),
>         BPF_JMP_IMM(BPF_JSLT, BPF_REG_0, 0, 2),
>         BPF_MOV64_IMM(BPF_REG_0, -1),
>         BPF_EXIT_INSN(),
>         BPF_MOV64_IMM(BPF_REG_0, 0),
>         BPF_EXIT_INSN(),
>         },
>         /* Use prog type that requires return value in range [0, 1] */
>         .prog_type = BPF_PROG_TYPE_SK_LOOKUP,
>         .expected_attach_type = BPF_SK_LOOKUP,
>         .result = VERBOSE_ACCEPT,
>         .runs = -1,
>         .errstr = "0: (7a) *(u64 *)(r10 -8) = -44        ; R10=fp0 fp-8_w=-44\
>         2: (c5) if r0 s< 0x0 goto pc+2\
>         2: R0_w=-44",
> },