From: Yonghong Song <yhs@fb.com>
To: Daniel Borkmann <daniel@iogearbox.net>,
"ast@kernel.org" <ast@kernel.org>
Cc: "netdev@vger.kernel.org" <netdev@vger.kernel.org>,
"bpf@vger.kernel.org" <bpf@vger.kernel.org>,
"anatoly.trosinenko@gmail.com" <anatoly.trosinenko@gmail.com>
Subject: Re: [PATCH bpf] bpf: Fix incorrect verifier simulation of ARSH under ALU32
Date: Wed, 15 Jan 2020 21:30:57 +0000 [thread overview]
Message-ID: <51d3fb28-a9f9-1feb-74fb-9011ced98ffc@fb.com> (raw)
In-Reply-To: <20200115204733.16648-1-daniel@iogearbox.net>
On 1/15/20 12:47 PM, Daniel Borkmann wrote:
> Anatoly has been fuzzing with kBdysch harness and reported a hang in one
> of the outcomes:
>
> 0: R1=ctx(id=0,off=0,imm=0) R10=fp0
> 0: (85) call bpf_get_socket_cookie#46
> 1: R0_w=invP(id=0) R10=fp0
> 1: (57) r0 &= 808464432
> 2: R0_w=invP(id=0,umax_value=808464432,var_off=(0x0; 0x30303030)) R10=fp0
> 2: (14) w0 -= 810299440
> 3: R0_w=invP(id=0,umax_value=4294967295,var_off=(0xcf800000; 0x3077fff0)) R10=fp0
> 3: (c4) w0 s>>= 1
> 4: R0_w=invP(id=0,umin_value=1740636160,umax_value=2147221496,var_off=(0x67c00000; 0x183bfff8)) R10=fp0
> 4: (76) if w0 s>= 0x30303030 goto pc+216
> 221: R0_w=invP(id=0,umin_value=1740636160,umax_value=2147221496,var_off=(0x67c00000; 0x183bfff8)) R10=fp0
> 221: (95) exit
> processed 6 insns (limit 1000000) [...]
>
> Taking a closer look, the program was xlated as follows:
>
> # ./bpftool p d x i 12
> 0: (85) call bpf_get_socket_cookie#7800896
> 1: (bf) r6 = r0
> 2: (57) r6 &= 808464432
> 3: (14) w6 -= 810299440
> 4: (c4) w6 s>>= 1
> 5: (76) if w6 s>= 0x30303030 goto pc+216
> 6: (05) goto pc-1
> 7: (05) goto pc-1
> 8: (05) goto pc-1
> [...]
> 220: (05) goto pc-1
> 221: (05) goto pc-1
> 222: (95) exit
>
> Meaning, the visible effect is very similar to f54c7898ed1c ("bpf: Fix
> precision tracking for unbounded scalars"), that is, the fall-through
> branch in the instruction 5 is considered to be never taken given the
> conclusion from the min/max bounds tracking in w6, and therefore the
> dead-code sanitation rewrites it as goto pc-1. However, real-life input
> disagrees with verification analysis since a soft-lockup was observed.
>
> The bug sits in the analysis of the ARSH. The definition is that we shift
> the target register value right by K bits through shifting in copies of
> its sign bit. In adjust_scalar_min_max_vals(), we do first coerce the
> register into 32 bit mode, same happens after simulating the operation.
> However, for the case of simulating the actual ARSH, we don't take the
> mode into account and act as if it's always 64 bit, but location of sign
> bit is different:
>
> dst_reg->smin_value >>= umin_val;
> dst_reg->smax_value >>= umin_val;
> dst_reg->var_off = tnum_arshift(dst_reg->var_off, umin_val);
>
> Consider an unknown R0 where bpf_get_socket_cookie() (or others) would
> for example return 0xffff. With the above ARSH simulation, we'd see the
> following results:
>
> [...]
> 1: R1=ctx(id=0,off=0,imm=0) R2_w=invP65535 R10=fp0
> 1: (85) call bpf_get_socket_cookie#46
> 2: R0_w=invP(id=0) R10=fp0
> 2: (57) r0 &= 808464432
> -> R0_runtime = 0x3030
> 3: R0_w=invP(id=0,umax_value=808464432,var_off=(0x0; 0x30303030)) R10=fp0
> 3: (14) w0 -= 810299440
> -> R0_runtime = 0xcfb40000
> 4: R0_w=invP(id=0,umax_value=4294967295,var_off=(0xcf800000; 0x3077fff0)) R10=fp0
> (0xffffffff)
> 4: (c4) w0 s>>= 1
> -> R0_runtime = 0xe7da0000
> 5: R0_w=invP(id=0,umin_value=1740636160,umax_value=2147221496,var_off=(0x67c00000; 0x183bfff8)) R10=fp0
> (0x67c00000) (0x7ffbfff8)
> [...]
>
> In insn 3, we have a runtime value of 0xcfb40000, which is '1100 1111 1011
> 0100 0000 0000 0000 0000', the result after the shift has 0xe7da0000 that
> is '1110 0111 1101 1010 0000 0000 0000 0000', where the sign bit is correctly
> retained in 32 bit mode. In insn4, the umax was 0xffffffff, and changed into
> 0x7ffbfff8 after the shift, that is, '0111 1111 1111 1011 1111 1111 1111 1000'
> and means here that the simulation didn't retain the sign bit. With above
> logic, the updates happen on the 64 bit min/max bounds and given we coerced
> the register, the sign bits of the bounds are cleared as well, meaning, we
> need to force the simulation into s32 space for 32 bit alu mode.
>
> Verification after the fix below. We're first analyzing the fall-through branch
> on 32 bit signed >= test eventually leading to rejection of the program in this
> specific case:
>
> 0: R1=ctx(id=0,off=0,imm=0) R10=fp0
> 0: (b7) r2 = 808464432
> 1: R1=ctx(id=0,off=0,imm=0) R2_w=invP808464432 R10=fp0
> 1: (85) call bpf_get_socket_cookie#46
> 2: R0_w=invP(id=0) R10=fp0
> 2: (bf) r6 = r0
> 3: R0_w=invP(id=0) R6_w=invP(id=0) R10=fp0
> 3: (57) r6 &= 808464432
> 4: R0_w=invP(id=0) R6_w=invP(id=0,umax_value=808464432,var_off=(0x0; 0x30303030)) R10=fp0
> 4: (14) w6 -= 810299440
> 5: R0_w=invP(id=0) R6_w=invP(id=0,umax_value=4294967295,var_off=(0xcf800000; 0x3077fff0)) R10=fp0
> 5: (c4) w6 s>>= 1
> 6: R0_w=invP(id=0) R6_w=invP(id=0,umin_value=3888119808,umax_value=4294705144,var_off=(0xe7c00000; 0x183bfff8)) R10=fp0
> (0x67c00000) (0xfffbfff8)
> 6: (76) if w6 s>= 0x30303030 goto pc+216
> 7: R0_w=invP(id=0) R6_w=invP(id=0,umin_value=3888119808,umax_value=4294705144,var_off=(0xe7c00000; 0x183bfff8)) R10=fp0
> 7: (30) r0 = *(u8 *)skb[808464432]
> BPF_LD_[ABS|IND] uses reserved fields
> processed 8 insns (limit 1000000) [...]
>
> Fixes: 9cbe1f5a32dc ("bpf/verifier: improve register value range tracking with ARSH")
> Reported-by: Anatoly Trosinenko <anatoly.trosinenko@gmail.com>
> Signed-off-by: Daniel Borkmann <daniel@iogearbox.net>
Acked-by: Yonghong Song <yhs@fb.com>
next prev parent reply other threads:[~2020-01-15 21:31 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-01-15 20:47 [PATCH bpf] bpf: Fix incorrect verifier simulation of ARSH under ALU32 Daniel Borkmann
2020-01-15 21:30 ` Yonghong Song [this message]
2020-01-15 21:41 ` Alexei Starovoitov
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=51d3fb28-a9f9-1feb-74fb-9011ced98ffc@fb.com \
--to=yhs@fb.com \
--cc=anatoly.trosinenko@gmail.com \
--cc=ast@kernel.org \
--cc=bpf@vger.kernel.org \
--cc=daniel@iogearbox.net \
--cc=netdev@vger.kernel.org \
/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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).