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

[Andrii Nakryiko]

On Tue, Nov 28, 2023 at 11:44 PM Hao Sun <sunhao.th@xxxxxxxxx> wrote:
>
> On Wed, Nov 29, 2023 at 6:43 AM Andrii Nakryiko
> <andrii.nakryiko@xxxxxxxxx> wrote:
> >
> > On Tue, Nov 21, 2023 at 7:08 AM Hao Sun <sunhao.th@xxxxxxxxx> 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
> >

No, it actually is fine. We know that lower 32 bits are exactly
0xfffffffe (-2), and we propagate that into smin/smax, which are
narrowed from [0x80....00, 0x7ffff...ff] to [0x80000000fffffffe,
0x7ffffffffffffffe]. This all looks correct so far. This is not the
issue.


> > > 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.
> >
>
> Yes, I'm aware of that, which is why I only selected two suspicious cases
> to report. Also, this is true after the check (5f99f312bd3be: bpf: add
> register bounds sanity checks and sanitization), but these cases may
> cause some issues in the previous releases. Your recent improvement in
> return value check also helps.
>
> I will see what I can do, maybe add more checks by using both tnum and
> ranges information in is_scalar_branch_taken().
>
> Thanks!

Ok, so I did take a look at this over last two days as well. There is
indeed a problem, and it's basically another variation on the same
issue: getting to the point of two disjoint ranges. Here's the repro
program in the form that's easy to compile and work with with
veristat:

+// SPDX-License-Identifier: GPL-2.0
+/* Copyright (C) 2023 SUSE LLC */
+#include <linux/bpf.h>
+#include <bpf/bpf_helpers.h>
+#include "bpf_misc.h"
+
+SEC("?raw_tp")
+__success __log_level(2)
+__naked int bpf_blah(void)
+{
+       asm volatile (
+               "r0 = -2;"
+               "r0 /= 1;"
+               "r8 = r0;"
+               "if w8 != 0xfffffffe goto 1f;"
+               "if r8 s> 0xd goto 1f;"
+               "r4 = 2;"
+               "if r8 s<= r4 goto 1f;"
+               "w8 s>>= w0;"
+       "1:"
+               "r0 >>= 32;"
+               "r0 &= 1;"
+               "exit;"
+               ::: __clobber_all);
+}
+
+char _license[] SEC("license") = "GPL";


The problem here is that we end up with the state of r8 before `if r8
s<= r4` (r4 is just 2, simple) where we estimate that 32-bit
subregister is -2 (0xfffffffe), while full smin/smax is some
0x8000....fffffe stuff. And so when we do comparison, we end up with
smin/smax estimate that is disjoint with 0xfffffffe (it's [3, 13] or
something like that in the fall through case). tnum is also
interferes, btw.

Anyways. I tried some ideas on how to prevent this. One of them is to
forget about 32-bit and opposite signedness estimates and re-derive
them in reg_bounds_sync(). The code below achieves this, but it breaks
a ton of other tests that expect tighter bounds. So it's not really a
solution, but I'll leave it below just to give an idea.

In short, this simultaneous 5 domain representation we use in register
state (tnum + s64 + u64 + s32 + u32) is really tricky to get right in
*all* possible cases, there are highly non-trivial interactions.
Perhaps someone can come up with the "unifying" implementation that
will be perfect, but for now reg_bounds_sanity_check() gives us a bit
of a safety net, at least.


commit 285068a77ca4e856faf695b41d17d7b5347ded0d (HEAD -> bpf-reg-bounds-debug)
Author: Andrii Nakryiko <andrii@xxxxxxxxxx>
Date:   Wed Dec 13 09:27:22 2023 -0800

    bpf: reset irrelevant numeric domains in inequality conditionals

    Forfeit previous knowledge of other numeric domains, as they become
    invalidated anyways. If we don't reset them, they can bite us back with
    at best irrelevant and at worst wrong range estimates.

    Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx>

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index bb64203c5d89..dc3aaed15940 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -1911,6 +1911,34 @@ static void __mark_reg32_unbounded(struct
bpf_reg_state *reg)
        reg->u32_max_value = U32_MAX;
 }

+static void __mark_reg32_signed_unbounded(struct bpf_reg_state *reg)
+{
+       reg->s32_min_value = S32_MIN;
+       reg->s32_max_value = S32_MAX;
+       reg->var_off = tnum_with_subreg(reg->var_off, tnum_unknown);
+}
+
+static void __mark_reg32_unsigned_unbounded(struct bpf_reg_state *reg)
+{
+       reg->u32_min_value = 0;
+       reg->u32_max_value = U32_MAX;
+       reg->var_off = tnum_with_subreg(reg->var_off, tnum_unknown);
+}
+
+static void __mark_reg64_signed_unbounded(struct bpf_reg_state *reg)
+{
+       reg->smin_value = S64_MIN;
+       reg->smax_value = S64_MAX;
+       reg->var_off = tnum_unknown;
+}
+
+static void __mark_reg64_unsigned_unbounded(struct bpf_reg_state *reg)
+{
+       reg->umin_value = 0;
+       reg->umax_value = U64_MAX;
+       reg->var_off = tnum_unknown;
+}
+
 static void __update_reg32_bounds(struct bpf_reg_state *reg)
 {
        struct tnum var32_off = tnum_subreg(reg->var_off);
@@ -14409,36 +14437,60 @@ static void regs_refine_cond_op(struct
bpf_reg_state *reg1, struct bpf_reg_state
                if (is_jmp32) {
                        reg1->u32_max_value = min(reg1->u32_max_value,
reg2->u32_max_value);
                        reg2->u32_min_value = max(reg1->u32_min_value,
reg2->u32_min_value);
+                       __mark_reg32_signed_unbounded(reg1);
+                       __mark_reg32_signed_unbounded(reg2);
                } else {
                        reg1->umax_value = min(reg1->umax_value,
reg2->umax_value);
                        reg2->umin_value = max(reg1->umin_value,
reg2->umin_value);
+                       __mark_reg64_signed_unbounded(reg1);
+                       __mark_reg64_signed_unbounded(reg2);
+                       __mark_reg32_unbounded(reg1);
+                       __mark_reg32_unbounded(reg2);
                }
                break;
        case BPF_JLT:
                if (is_jmp32) {
                        reg1->u32_max_value = min(reg1->u32_max_value,
reg2->u32_max_value - 1);
                        reg2->u32_min_value = max(reg1->u32_min_value
+ 1, reg2->u32_min_value);
+                       __mark_reg32_signed_unbounded(reg1);
+                       __mark_reg32_signed_unbounded(reg2);
                } else {
                        reg1->umax_value = min(reg1->umax_value,
reg2->umax_value - 1);
                        reg2->umin_value = max(reg1->umin_value + 1,
reg2->umin_value);
+                       __mark_reg64_signed_unbounded(reg1);
+                       __mark_reg64_signed_unbounded(reg2);
+                       __mark_reg32_unbounded(reg1);
+                       __mark_reg32_unbounded(reg2);
                }
                break;
        case BPF_JSLE:
                if (is_jmp32) {
                        reg1->s32_max_value = min(reg1->s32_max_value,
reg2->s32_max_value);
                        reg2->s32_min_value = max(reg1->s32_min_value,
reg2->s32_min_value);
+                       __mark_reg32_unsigned_unbounded(reg1);
+                       __mark_reg32_unsigned_unbounded(reg2);
                } else {
                        reg1->smax_value = min(reg1->smax_value,
reg2->smax_value);
                        reg2->smin_value = max(reg1->smin_value,
reg2->smin_value);
+                       __mark_reg64_unsigned_unbounded(reg1);
+                       __mark_reg64_unsigned_unbounded(reg2);
+                       __mark_reg32_unbounded(reg1);
+                       __mark_reg32_unbounded(reg2);
                }
                break;
        case BPF_JSLT:
                if (is_jmp32) {
                        reg1->s32_max_value = min(reg1->s32_max_value,
reg2->s32_max_value - 1);
                        reg2->s32_min_value = max(reg1->s32_min_value
+ 1, reg2->s32_min_value);
+                       __mark_reg32_unsigned_unbounded(reg1);
+                       __mark_reg32_unsigned_unbounded(reg2);
                } else {
                        reg1->smax_value = min(reg1->smax_value,
reg2->smax_value - 1);
                        reg2->smin_value = max(reg1->smin_value + 1,
reg2->smin_value);
+                       __mark_reg64_unsigned_unbounded(reg1);
+                       __mark_reg64_unsigned_unbounded(reg2);
+                       __mark_reg32_unbounded(reg1);
+                       __mark_reg32_unbounded(reg2);
                }
                break;
        case BPF_JGE: