From: John Fastabend <john.fastabend@gmail.com>
To: Daniel Borkmann <daniel@iogearbox.net>, bpf@vger.kernel.org
Cc: Daniel Borkmann <daniel@iogearbox.net>,
Xu Kuohai <xukuohai@huaweicloud.com>,
John Fastabend <john.fastabend@gmail.com>,
Eduard Zingerman <eddyz87@gmail.com>
Subject: RE: [PATCH bpf-next 1/2] bpf: Fix __reg_bound_offset 64->32 var_off subreg propagation
Date: Tue, 21 Mar 2023 15:19:44 -0700 [thread overview]
Message-ID: <641a2d807e5a2_80a24208ec@john.notmuch> (raw)
In-Reply-To: <20230321193354.10445-1-daniel@iogearbox.net>
Daniel Borkmann wrote:
> Xu reports that after commit 3f50f132d840 ("bpf: Verifier, do explicit ALU32
> bounds tracking"), the following BPF program is rejected by the verifier:
>
> 0: (61) r2 = *(u32 *)(r1 +0) ; R2_w=pkt(off=0,r=0,imm=0)
> 1: (61) r3 = *(u32 *)(r1 +4) ; R3_w=pkt_end(off=0,imm=0)
> 2: (bf) r1 = r2
> 3: (07) r1 += 1
> 4: (2d) if r1 > r3 goto pc+8
> 5: (71) r1 = *(u8 *)(r2 +0) ; R1_w=scalar(umax=255,var_off=(0x0; 0xff))
> 6: (18) r0 = 0x7fffffffffffff10
> 8: (0f) r1 += r0 ; R1_w=scalar(umin=0x7fffffffffffff10,umax=0x800000000000000f)
> 9: (18) r0 = 0x8000000000000000
> 11: (07) r0 += 1
> 12: (ad) if r0 < r1 goto pc-2
> 13: (b7) r0 = 0
> 14: (95) exit
>
> And the verifier log says:
>
> func#0 @0
> 0: R1=ctx(off=0,imm=0) R10=fp0
> 0: (61) r2 = *(u32 *)(r1 +0) ; R1=ctx(off=0,imm=0) R2_w=pkt(off=0,r=0,imm=0)
> 1: (61) r3 = *(u32 *)(r1 +4) ; R1=ctx(off=0,imm=0) R3_w=pkt_end(off=0,imm=0)
> 2: (bf) r1 = r2 ; R1_w=pkt(off=0,r=0,imm=0) R2_w=pkt(off=0,r=0,imm=0)
> 3: (07) r1 += 1 ; R1_w=pkt(off=1,r=0,imm=0)
> 4: (2d) if r1 > r3 goto pc+8 ; R1_w=pkt(off=1,r=1,imm=0) R3_w=pkt_end(off=0,imm=0)
> 5: (71) r1 = *(u8 *)(r2 +0) ; R1_w=scalar(umax=255,var_off=(0x0; 0xff)) R2_w=pkt(off=0,r=1,imm=0)
> 6: (18) r0 = 0x7fffffffffffff10 ; R0_w=9223372036854775568
> 8: (0f) r1 += r0 ; R0_w=9223372036854775568 R1_w=scalar(umin=9223372036854775568,umax=9223372036854775823,s32_min=-240,s32_max=15)
> 9: (18) r0 = 0x8000000000000000 ; R0_w=-9223372036854775808
> 11: (07) r0 += 1 ; R0_w=-9223372036854775807
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775807 R1_w=scalar(umin=9223372036854775568,umax=9223372036854775809)
> 13: (b7) r0 = 0 ; R0_w=0
> 14: (95) exit
>
> from 12 to 11: R0_w=-9223372036854775807 R1_w=scalar(umin=9223372036854775810,umax=9223372036854775823,var_off=(0x8000000000000000; 0xffffffff)) R2_w=pkt(off=0,r=1,imm=0) R3_w=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775806
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775806 R1_w=scalar(umin=9223372036854775810,umax=9223372036854775810,var_off=(0x8000000000000000; 0xffffffff))
> 13: safe
>
> [...]
>
> from 12 to 11: R0_w=-9223372036854775795 R1=scalar(umin=9223372036854775822,umax=9223372036854775823,var_off=(0x8000000000000000; 0xffffffff)) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775794
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775794 R1=scalar(umin=9223372036854775822,umax=9223372036854775822,var_off=(0x8000000000000000; 0xffffffff))
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775794 R1=scalar(umin=9223372036854775823,umax=9223372036854775823,var_off=(0x8000000000000000; 0xffffffff)) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775793
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775793 R1=scalar(umin=9223372036854775823,umax=9223372036854775823,var_off=(0x8000000000000000; 0xffffffff))
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775793 R1=scalar(umin=9223372036854775824,umax=9223372036854775823,var_off=(0x8000000000000000; 0xffffffff)) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775792
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775792 R1=scalar(umin=9223372036854775824,umax=9223372036854775823,var_off=(0x8000000000000000; 0xffffffff))
> 13: safe
>
> [...]
>
> The 64bit umin=9223372036854775810 bound continuously bumps by +1 while
> umax=9223372036854775823 stays as-is until the verifier complexity limit
> is reached and the program gets finally rejected. During this simulation,
> the umin also eventually surpasses umax. Looking at the first 'from 12
> to 11' output line from the loop, R1 has the following state:
>
> R1_w=scalar(umin=0x8000000000000002 (9223372036854775810),
> umax=0x800000000000000f (9223372036854775823),
> var_off=(0x8000000000000000;
> 0xffffffff))
>
> The var_off has technically not an inconsistent state but it's very
> imprecise and far off surpassing 64bit umax bounds whereas the expected
> output refining bits in var_off should have been like:
>
> R1_w=scalar(umin=0x8000000000000002 (9223372036854775810),
> umax=0x800000000000000f (9223372036854775823),
> var_off=(0x8000000000000000;
> 0xf))
>
> In the above log, var_off stays as var_off=(0x8000000000000000; 0xffffffff)
> and does not converge into a narrower mask where more bits become known,
> eventually transforming R1 into a constant upon umin=9223372036854775823,
> umax=9223372036854775823 case where the verifier would have terminated and
> let the program pass.
>
> The __reg_combine_64_into_32() marks the subregister unknown and propagates
> 64bit {s,u}min/{s,u}max bounds to their 32bit equivalents iff they are within
> the 32bit universe. The question came up whether __reg_combine_64_into_32()
> should special case the situation that when 64bit {s,u}min bounds have
> the same value as 64bit {s,u}max bounds to then assign the latter as
> well to the 32bit reg->{s,u}32_{min,max}_value. As can be seen from the
> above example however, that is just /one/ special case and not a /generic/
> solution given above example would still not be addressed this way and
> remain at an imprecise var_off=(0x8000000000000000; 0xffffffff).
>
> The improvement is needed in __reg_bound_offset() to refine var32_off with
> the updated var64_off instead of the prior reg->var_off. The reg_bounds_sync()
> code first refines information about the register's min/max bounds via
> __update_reg_bounds() from the current var_off, then in __reg_deduce_bounds()
> from sign bit and with the potentially learned bits from bounds it'll
> update the var_off tnum in __reg_bound_offset(). For example, intersecting
> with the old var_off might have improved bounds slightly, e.g. if umax
> was 0x7f...f and var_off was (0; 0xf...fc), then new var_off will then
> result in (0; 0x7f...fc). The intersected var64_off holds then the
> universe which is a superset of var32_off. The point for the latter is
> not to broaden, but to further refine known bits based on the intersection
> of var_off with 32 bit bounds, so that we later construct the final var_off
> from upper and lower 32 bits. The final __update_reg_bounds() can then
> potentially refine bounds if more bits became known from new var_off.
>
> After the improvement, we can see R1 converging successively:
>
> func#0 @0
> 0: R1=ctx(off=0,imm=0) R10=fp0
> 0: (61) r2 = *(u32 *)(r1 +0) ; R1=ctx(off=0,imm=0) R2_w=pkt(off=0,r=0,imm=0)
> 1: (61) r3 = *(u32 *)(r1 +4) ; R1=ctx(off=0,imm=0) R3_w=pkt_end(off=0,imm=0)
> 2: (bf) r1 = r2 ; R1_w=pkt(off=0,r=0,imm=0) R2_w=pkt(off=0,r=0,imm=0)
> 3: (07) r1 += 1 ; R1_w=pkt(off=1,r=0,imm=0)
> 4: (2d) if r1 > r3 goto pc+8 ; R1_w=pkt(off=1,r=1,imm=0) R3_w=pkt_end(off=0,imm=0)
> 5: (71) r1 = *(u8 *)(r2 +0) ; R1_w=scalar(umax=255,var_off=(0x0; 0xff)) R2_w=pkt(off=0,r=1,imm=0)
> 6: (18) r0 = 0x7fffffffffffff10 ; R0_w=9223372036854775568
> 8: (0f) r1 += r0 ; R0_w=9223372036854775568 R1_w=scalar(umin=9223372036854775568,umax=9223372036854775823,s32_min=-240,s32_max=15)
> 9: (18) r0 = 0x8000000000000000 ; R0_w=-9223372036854775808
> 11: (07) r0 += 1 ; R0_w=-9223372036854775807
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775807 R1_w=scalar(umin=9223372036854775568,umax=9223372036854775809)
> 13: (b7) r0 = 0 ; R0_w=0
> 14: (95) exit
>
> from 12 to 11: R0_w=-9223372036854775807 R1_w=scalar(umin=9223372036854775810,umax=9223372036854775823,var_off=(0x8000000000000000; 0xf),s32_min=0,s32_max=15,u32_max=15) R2_w=pkt(off=0,r=1,imm=0) R3_w=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775806
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775806 R1_w=-9223372036854775806
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775806 R1_w=scalar(umin=9223372036854775811,umax=9223372036854775823,var_off=(0x8000000000000000; 0xf),s32_min=0,s32_max=15,u32_max=15) R2_w=pkt(off=0,r=1,imm=0) R3_w=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775805
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775805 R1_w=-9223372036854775805
> 13: safe
>
> [...]
>
> from 12 to 11: R0_w=-9223372036854775798 R1=scalar(umin=9223372036854775819,umax=9223372036854775823,var_off=(0x8000000000000008; 0x7),s32_min=8,s32_max=15,u32_min=8,u32_max=15) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775797
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775797 R1=-9223372036854775797
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775797 R1=scalar(umin=9223372036854775820,umax=9223372036854775823,var_off=(0x800000000000000c; 0x3),s32_min=12,s32_max=15,u32_min=12,u32_max=15) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775796
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775796 R1=-9223372036854775796
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775796 R1=scalar(umin=9223372036854775821,umax=9223372036854775823,var_off=(0x800000000000000c; 0x3),s32_min=12,s32_max=15,u32_min=12,u32_max=15) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775795
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775795 R1=-9223372036854775795
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775795 R1=scalar(umin=9223372036854775822,umax=9223372036854775823,var_off=(0x800000000000000e; 0x1),s32_min=14,s32_max=15,u32_min=14,u32_max=15) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775794
> 12: (ad) if r0 < r1 goto pc-2 ; R0_w=-9223372036854775794 R1=-9223372036854775794
> 13: safe
>
> from 12 to 11: R0_w=-9223372036854775794 R1=-9223372036854775793 R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> 11: (07) r0 += 1 ; R0_w=-9223372036854775793
> 12: (ad) if r0 < r1 goto pc-2
> last_idx 12 first_idx 12
> parent didn't have regs=1 stack=0 marks: R0_rw=P-9223372036854775801 R1_r=scalar(umin=9223372036854775815,umax=9223372036854775823,var_off=(0x8000000000000000; 0xf),s32_min=0,s32_max=15,u32_max=15) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> last_idx 11 first_idx 11
> regs=1 stack=0 before 11: (07) r0 += 1
> parent didn't have regs=1 stack=0 marks: R0_rw=P-9223372036854775805 R1_rw=scalar(umin=9223372036854775812,umax=9223372036854775823,var_off=(0x8000000000000000; 0xf),s32_min=0,s32_max=15,u32_max=15) R2_w=pkt(off=0,r=1,imm=0) R3_w=pkt_end(off=0,imm=0) R10=fp0
> last_idx 12 first_idx 0
> regs=1 stack=0 before 12: (ad) if r0 < r1 goto pc-2
> regs=1 stack=0 before 11: (07) r0 += 1
> regs=1 stack=0 before 12: (ad) if r0 < r1 goto pc-2
> regs=1 stack=0 before 11: (07) r0 += 1
> regs=1 stack=0 before 12: (ad) if r0 < r1 goto pc-2
> regs=1 stack=0 before 11: (07) r0 += 1
> regs=1 stack=0 before 9: (18) r0 = 0x8000000000000000
> last_idx 12 first_idx 12
> parent didn't have regs=2 stack=0 marks: R0_rw=P-9223372036854775801 R1_r=Pscalar(umin=9223372036854775815,umax=9223372036854775823,var_off=(0x8000000000000000; 0xf),s32_min=0,s32_max=15,u32_max=15) R2=pkt(off=0,r=1,imm=0) R3=pkt_end(off=0,imm=0) R10=fp0
> last_idx 11 first_idx 11
> regs=2 stack=0 before 11: (07) r0 += 1
> parent didn't have regs=2 stack=0 marks: R0_rw=P-9223372036854775805 R1_rw=Pscalar(umin=9223372036854775812,umax=9223372036854775823,var_off=(0x8000000000000000; 0xf),s32_min=0,s32_max=15,u32_max=15) R2_w=pkt(off=0,r=1,imm=0) R3_w=pkt_end(off=0,imm=0) R10=fp0
> last_idx 12 first_idx 0
> regs=2 stack=0 before 12: (ad) if r0 < r1 goto pc-2
> regs=2 stack=0 before 11: (07) r0 += 1
> regs=2 stack=0 before 12: (ad) if r0 < r1 goto pc-2
> regs=2 stack=0 before 11: (07) r0 += 1
> regs=2 stack=0 before 12: (ad) if r0 < r1 goto pc-2
> regs=2 stack=0 before 11: (07) r0 += 1
> regs=2 stack=0 before 9: (18) r0 = 0x8000000000000000
> regs=2 stack=0 before 8: (0f) r1 += r0
> regs=3 stack=0 before 6: (18) r0 = 0x7fffffffffffff10
> regs=2 stack=0 before 5: (71) r1 = *(u8 *)(r2 +0)
> 13: safe
>
> from 4 to 13: safe
> verification time 322 usec
> stack depth 0
> processed 56 insns (limit 1000000) max_states_per_insn 1 total_states 3 peak_states 3 mark_read 1
>
> Fixes: 3f50f132d840 ("bpf: Verifier, do explicit ALU32 bounds tracking")
> Reported-by: Xu Kuohai <xukuohai@huaweicloud.com>
> Signed-off-by: Daniel Borkmann <daniel@iogearbox.net>
> Cc: John Fastabend <john.fastabend@gmail.com>
> Cc: Eduard Zingerman <eddyz87@gmail.com>
> Link: https://lore.kernel.org/bpf/20230314203424.4015351-2-xukuohai@huaweicloud.com
> ---
> kernel/bpf/verifier.c | 6 +++---
> 1 file changed, 3 insertions(+), 3 deletions(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index d517d13878cf..d66e70707172 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -1823,9 +1823,9 @@ static void __reg_bound_offset(struct bpf_reg_state *reg)
> struct tnum var64_off = tnum_intersect(reg->var_off,
> tnum_range(reg->umin_value,
> reg->umax_value));
> - struct tnum var32_off = tnum_intersect(tnum_subreg(reg->var_off),
> - tnum_range(reg->u32_min_value,
> - reg->u32_max_value));
> + struct tnum var32_off = tnum_intersect(tnum_subreg(var64_off),
> + tnum_range(reg->u32_min_value,
> + reg->u32_max_value));
>
> reg->var_off = tnum_or(tnum_clear_subreg(var64_off), var32_off);
> }
> --
> 2.27.0
>
LGTM this was just an oversight in the original patch.
Reviewed-by: John Fastabend <john.fastabend@gmail.com>
next prev parent reply other threads:[~2023-03-21 22:19 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2023-03-21 19:33 [PATCH bpf-next 1/2] bpf: Fix __reg_bound_offset 64->32 var_off subreg propagation Daniel Borkmann
2023-03-21 19:33 ` [PATCH bpf-next 2/2] selftests/bpf: Check when bounds are not in the 32-bit range Daniel Borkmann
2023-03-21 22:20 ` John Fastabend
2023-03-21 22:19 ` John Fastabend [this message]
2023-03-22 3:03 ` [PATCH bpf-next 1/2] bpf: Fix __reg_bound_offset 64->32 var_off subreg propagation Alexei Starovoitov
2023-03-22 7:44 ` Daniel Borkmann
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=641a2d807e5a2_80a24208ec@john.notmuch \
--to=john.fastabend@gmail.com \
--cc=bpf@vger.kernel.org \
--cc=daniel@iogearbox.net \
--cc=eddyz87@gmail.com \
--cc=xukuohai@huaweicloud.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.