linux-kernel - Re: [Bug Report] bpf: reg invariant voilation after JSLE

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Date:   Tue, 28 Nov 2023 21:42:52 -0800
From:   Andrii Nakryiko <andrii.nakryiko@...il.com>
To:     Hao Sun <sunhao.th@...il.com>
Cc:     Andrii Nakryiko <andrii@...nel.org>,
        Alexei Starovoitov <ast@...nel.org>,
        Daniel Borkmann <daniel@...earbox.net>,
        John Fastabend <john.fastabend@...il.com>,
        Martin KaFai Lau <martin.lau@...ux.dev>,
        Song Liu <song@...nel.org>,
        Yonghong Song <yonghong.song@...ux.dev>,
        KP Singh <kpsingh@...nel.org>,
        Stanislav Fomichev <sdf@...gle.com>,
        Jiri Olsa <jolsa@...nel.org>, bpf <bpf@...r.kernel.org>,
        Linux Kernel Mailing List <linux-kernel@...r.kernel.org>
Subject: Re: [Bug Report] bpf: reg invariant voilation after JSLE

On Tue, Nov 21, 2023 at 7:08 AM Hao Sun <sunhao.th@...il.com> wrote:
>
> Hi,
>
> The following program (reduced) breaks reg invariant:
>
> C Repro: https://pastebin.com/raw/SRQJYx91
>
> -------- Verifier Log --------
> func#0 @0
> 0: R1=ctx() R10=fp0
> 0: (b7) r0 = -2                       ; R0_w=-2
> 1: (37) r0 /= 1                       ; R0_w=scalar()
> 2: (bf) r8 = r0                       ; R0_w=scalar(id=1) R8_w=scalar(id=1)
> 3: (56) if w8 != 0xfffffffe goto pc+4         ;
> R8_w=scalar(id=1,smin=0x80000000fffffffe,smax=0x7ffffffffffffffe,umin=umin32=0xfffffffe,umax=0xfffffffffffffffe,smin32=-2,smax32=-2,umax32=0xfffffffe,var_off=(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=scalar(id=1,smin=0x80000000fffffffe,smax=13,umin=umin32=0xfffffffe,umax=0xfffffffffffffffe,smin32=-2,smax32=-2,umax32=0xfffffffe,var_off=(0xfffffffe;
> 0xffffffff00000000))
> 5: (b7) r4 = 2                        ; R4_w=2
> 6: (dd) if r8 s<= r4 goto pc+1
> REG INVARIANTS VIOLATION (false_reg1): range bounds violation
> u64=[0xfffffffe, 0xd] s64=[0xfffffffe, 0xd] u32=[0xfffffffe, 0xd]
> s32=[0x3, 0xfffffffe] var_off=(0xfffffffe, 0x0)
> 6: R4_w=2 R8_w=0xfffffffe
> 7: (cc) w8 s>>= w0                    ; R0=0xfffffffe R8=scalar()
> 8: (77) r0 >>= 32                     ; R0_w=0
> 9: (57) r0 &= 1                       ; R0_w=0
> 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