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:
