Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.38 as permitted sender) client-ip=23.128.96.38;
MIME-Version: 1.0
References: <CACkBjsaecr+VjmfOHzaMbiei5G3WMDjvjp4kZVE79Bn8ib1-Rg@mail.gmail.com>
In-Reply-To: <CACkBjsaecr+VjmfOHzaMbiei5G3WMDjvjp4kZVE79Bn8ib1-Rg@mail.gmail.com>
From:   Andrii Nakryiko <andrii.nakryiko@gmail.com>
Date:   Tue, 28 Nov 2023 21:42:52 -0800
Message-ID: <CAEf4BzYVRwpP6TbXdJeFwMot80FodexyOk2_Y9H2tsJC-3FBUA@mail.gmail.com>
Subject: Re: [Bug Report] bpf: reg invariant voilation after JSLE
To:     Hao Sun <sunhao.th@gmail.com>
Cc:     Andrii Nakryiko <andrii@kernel.org>,
        Alexei Starovoitov <ast@kernel.org>,
        Daniel Borkmann <daniel@iogearbox.net>,
        John Fastabend <john.fastabend@gmail.com>,
        Martin KaFai Lau <martin.lau@linux.dev>,
        Song Liu <song@kernel.org>,
        Yonghong Song <yonghong.song@linux.dev>,
        KP Singh <kpsingh@kernel.org>,
        Stanislav Fomichev <sdf@google.com>,
        Jiri Olsa <jolsa@kernel.org>, bpf <bpf@vger.kernel.org>,
        Linux Kernel Mailing List <linux-kernel@vger.kernel.org>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Precedence: bulk

On Tue, Nov 21, 2023 at 7:08=E2=80=AFAM Hao Sun <sunhao.th@gmail.com> wrote=
:
>
> Hi,
>
> The following program (reduced) breaks reg invariant:
>
> C Repro: https://pastebin.com/raw/SRQJYx91
>
> -------- Verifier Log --------
> func#0 @0
> 0: R1=3Dctx() R10=3Dfp0
> 0: (b7) r0 =3D -2                       ; R0_w=3D-2
> 1: (37) r0 /=3D 1                       ; R0_w=3Dscalar()
> 2: (bf) r8 =3D r0                       ; R0_w=3Dscalar(id=3D1) R8_w=3Dsc=
alar(id=3D1)
> 3: (56) if w8 !=3D 0xfffffffe goto pc+4         ;
> R8_w=3Dscalar(id=3D1,smin=3D0x80000000fffffffe,smax=3D0x7ffffffffffffffe,=
umin=3Dumin32=3D0xfffffffe,umax=3D0xfffffffffffffffe,smin32=3D-2,smax32=3D-=
2,umax32=3D0xfffffffe,var_off=3D(0xfffffffe;
> 0xffffffff00000000))

this part looks suspicious, I'll take a look a bit later

> 4: (65) if r8 s> 0xd goto pc+3        ;
> R8_w=3Dscalar(id=3D1,smin=3D0x80000000fffffffe,smax=3D13,umin=3Dumin32=3D=
0xfffffffe,umax=3D0xfffffffffffffffe,smin32=3D-2,smax32=3D-2,umax32=3D0xfff=
ffffe,var_off=3D(0xfffffffe;
> 0xffffffff00000000))
> 5: (b7) r4 =3D 2                        ; R4_w=3D2
> 6: (dd) if r8 s<=3D r4 goto pc+1
> REG INVARIANTS VIOLATION (false_reg1): range bounds violation
> u64=3D[0xfffffffe, 0xd] s64=3D[0xfffffffe, 0xd] u32=3D[0xfffffffe, 0xd]
> s32=3D[0x3, 0xfffffffe] var_off=3D(0xfffffffe, 0x0)
> 6: R4_w=3D2 R8_w=3D0xfffffffe
> 7: (cc) w8 s>>=3D w0                    ; R0=3D0xfffffffe R8=3Dscalar()
> 8: (77) r0 >>=3D 32                     ; R0_w=3D0
> 9: (57) r0 &=3D 1                       ; R0_w=3D0
> 10: (95) exit
>
> from 6 to 8: safe
>
> from 4 to 8: safe
>
> from 3 to 8: safe
> processed 14 insns (limit 1000000) max_states_per_insn 0 total_states
> 1 peak_states 1 mark_read 1
>
>
> Besides, the verifier enforces the return value of some prog types to
> be zero, the bug may lead to programs with arbitrary values loaded.

Generally speaking, if the verifier reports "REG INVARIANTS VIOLATION"
warning above, it doesn't necessarily mean that verifier has some bug.
We do know that in some conditions verifier doesn't detect conditions
that *will not* be taken, and in such cases we might get reg
invariants violation. But in such case verifier will revert to
conservative unknown scalar state, which is correct, even if
potentially unnecessarily pessimistic.

>
> Best
> Hao Sun