Hi,
The verifier incorrectly rejects the following prog in check_cfg() when
loading with root with confusing log `back-edge insn from 7 to 8`:
/* 0: r9 = 2
* 1: r3 = 0x20
* 2: r4 = 0x35
* 3: r8 = r4
* 4: goto+3
* 5: r9 -= r3
* 6: r9 -= r4
* 7: r9 -= r8
* 8: r8 += r4
* 9: if r8 < 0x64 goto-5
* 10: r0 = r9
* 11: exit
* */
BPF_MOV64_IMM(BPF_REG_9, 2),
BPF_MOV64_IMM(BPF_REG_3, 0x20),
BPF_MOV64_IMM(BPF_REG_4, 0x35),
BPF_MOV64_REG(BPF_REG_8, BPF_REG_4),
BPF_JMP_IMM(BPF_JA, 0, 0, 3),
BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_3),
BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_4),
BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_8),
BPF_ALU64_REG(BPF_ADD, BPF_REG_8, BPF_REG_4),
BPF_JMP32_IMM(BPF_JLT, BPF_REG_8, 0x68, -5),
BPF_MOV64_REG(BPF_REG_0, BPF_REG_9),
BPF_EXIT_INSN()
-------- Verifier Log --------
func#0 @0
back-edge from insn 7 to 8
processed 0 insns (limit 1000000) max_states_per_insn 0 total_states 0
peak_states 0 mark_read 0
This is not intentionally rejected, right?
Best
Hao
On Wed, Nov 1, 2023 at 6:56 AM Hao Sun <[email protected]> wrote:
>
> Hi,
>
> The verifier incorrectly rejects the following prog in check_cfg() when
> loading with root with confusing log `back-edge insn from 7 to 8`:
> /* 0: r9 = 2
> * 1: r3 = 0x20
> * 2: r4 = 0x35
> * 3: r8 = r4
> * 4: goto+3
> * 5: r9 -= r3
> * 6: r9 -= r4
> * 7: r9 -= r8
> * 8: r8 += r4
> * 9: if r8 < 0x64 goto-5
> * 10: r0 = r9
> * 11: exit
> * */
> BPF_MOV64_IMM(BPF_REG_9, 2),
> BPF_MOV64_IMM(BPF_REG_3, 0x20),
> BPF_MOV64_IMM(BPF_REG_4, 0x35),
> BPF_MOV64_REG(BPF_REG_8, BPF_REG_4),
> BPF_JMP_IMM(BPF_JA, 0, 0, 3),
> BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_3),
> BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_4),
> BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_8),
> BPF_ALU64_REG(BPF_ADD, BPF_REG_8, BPF_REG_4),
> BPF_JMP32_IMM(BPF_JLT, BPF_REG_8, 0x68, -5),
> BPF_MOV64_REG(BPF_REG_0, BPF_REG_9),
> BPF_EXIT_INSN()
>
> -------- Verifier Log --------
> func#0 @0
> back-edge from insn 7 to 8
> processed 0 insns (limit 1000000) max_states_per_insn 0 total_states 0
> peak_states 0 mark_read 0
>
> This is not intentionally rejected, right?
The way you wrote it, with goto +3, yes, it's intentional. Note that
you'll get different results in privileged and unprivileged modes.
Privileged mode allows "bounded loops" logic, so it doesn't
immediately reject this program, and then later sees that r8 is always
< 0x64, so program is correct.
But in unprivileged mode the rules are different, and this conditional
back edge is not allowed, which is probably what you are getting.
It's actually confusing and your "back-edge from insn 7 to 8" is out
of date and doesn't correspond to your program, you should see
"back-edge from insn 11 to 7", please double check.
Anyways, while I was looking into this, I realized that ldimm64 isn't
handled exactly correctly in check_cfg(), so I just sent a fix. It
also adds a nicer detection of jumping into the middle of the ldimm64
instruction, which I believe is something you were advocating for.
>
> Best
> Hao
On Wed, Nov 1, 2023 at 9:57 PM Andrii Nakryiko
<[email protected]> wrote:
>
> On Wed, Nov 1, 2023 at 6:56 AM Hao Sun <[email protected]> wrote:
> >
> > Hi,
> >
> > The verifier incorrectly rejects the following prog in check_cfg() when
> > loading with root with confusing log `back-edge insn from 7 to 8`:
> > /* 0: r9 = 2
> > * 1: r3 = 0x20
> > * 2: r4 = 0x35
> > * 3: r8 = r4
> > * 4: goto+3
> > * 5: r9 -= r3
> > * 6: r9 -= r4
> > * 7: r9 -= r8
> > * 8: r8 += r4
> > * 9: if r8 < 0x64 goto-5
> > * 10: r0 = r9
> > * 11: exit
> > * */
> > BPF_MOV64_IMM(BPF_REG_9, 2),
> > BPF_MOV64_IMM(BPF_REG_3, 0x20),
> > BPF_MOV64_IMM(BPF_REG_4, 0x35),
> > BPF_MOV64_REG(BPF_REG_8, BPF_REG_4),
> > BPF_JMP_IMM(BPF_JA, 0, 0, 3),
> > BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_3),
> > BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_4),
> > BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_8),
> > BPF_ALU64_REG(BPF_ADD, BPF_REG_8, BPF_REG_4),
> > BPF_JMP32_IMM(BPF_JLT, BPF_REG_8, 0x68, -5),
> > BPF_MOV64_REG(BPF_REG_0, BPF_REG_9),
> > BPF_EXIT_INSN()
> >
> > -------- Verifier Log --------
> > func#0 @0
> > back-edge from insn 7 to 8
> > processed 0 insns (limit 1000000) max_states_per_insn 0 total_states 0
> > peak_states 0 mark_read 0
> >
> > This is not intentionally rejected, right?
>
> The way you wrote it, with goto +3, yes, it's intentional. Note that
> you'll get different results in privileged and unprivileged modes.
> Privileged mode allows "bounded loops" logic, so it doesn't
> immediately reject this program, and then later sees that r8 is always
> < 0x64, so program is correct.
>
I load the program with privileged mode, and goto-5 makes the program
run from #9 to #5, so r8 is updated and the program is not infinite loop.
> But in unprivileged mode the rules are different, and this conditional
> back edge is not allowed, which is probably what you are getting.
>
> It's actually confusing and your "back-edge from insn 7 to 8" is out
> of date and doesn't correspond to your program, you should see
> "back-edge from insn 11 to 7", please double check.
>
Yes it's also confusing to me, but "back-edge from insn 7 to 8" is what
I got. The execution path of the program is #4 to #8 (goto+3), so the
verifier see the #8 first. Then, the program then goes #9 to #5 (goto-5),
the verifier thus sees #7 to #8 and incorrectly concludes back-edge here.
This can is the verifier log I got from latest bpf-next, this C program can
reproduce this: https://pastebin.com/raw/Yug0NVwx
> Anyways, while I was looking into this, I realized that ldimm64 isn't
> handled exactly correctly in check_cfg(), so I just sent a fix. It
> also adds a nicer detection of jumping into the middle of the ldimm64
> instruction, which I believe is something you were advocating for.
>
> >
> > Best
> > Hao
On Thu, Nov 2, 2023 at 3:30 AM Hao Sun <[email protected]> wrote:
>
> On Wed, Nov 1, 2023 at 9:57 PM Andrii Nakryiko
> <[email protected]> wrote:
> >
> > On Wed, Nov 1, 2023 at 6:56 AM Hao Sun <[email protected]> wrote:
> > >
> > > Hi,
> > >
> > > The verifier incorrectly rejects the following prog in check_cfg() when
> > > loading with root with confusing log `back-edge insn from 7 to 8`:
> > > /* 0: r9 = 2
> > > * 1: r3 = 0x20
> > > * 2: r4 = 0x35
> > > * 3: r8 = r4
> > > * 4: goto+3
> > > * 5: r9 -= r3
> > > * 6: r9 -= r4
> > > * 7: r9 -= r8
> > > * 8: r8 += r4
> > > * 9: if r8 < 0x64 goto-5
> > > * 10: r0 = r9
> > > * 11: exit
> > > * */
> > > BPF_MOV64_IMM(BPF_REG_9, 2),
> > > BPF_MOV64_IMM(BPF_REG_3, 0x20),
> > > BPF_MOV64_IMM(BPF_REG_4, 0x35),
> > > BPF_MOV64_REG(BPF_REG_8, BPF_REG_4),
> > > BPF_JMP_IMM(BPF_JA, 0, 0, 3),
> > > BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_3),
> > > BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_4),
> > > BPF_ALU64_REG(BPF_SUB, BPF_REG_9, BPF_REG_8),
> > > BPF_ALU64_REG(BPF_ADD, BPF_REG_8, BPF_REG_4),
> > > BPF_JMP32_IMM(BPF_JLT, BPF_REG_8, 0x68, -5),
> > > BPF_MOV64_REG(BPF_REG_0, BPF_REG_9),
> > > BPF_EXIT_INSN()
> > >
> > > -------- Verifier Log --------
> > > func#0 @0
> > > back-edge from insn 7 to 8
> > > processed 0 insns (limit 1000000) max_states_per_insn 0 total_states 0
> > > peak_states 0 mark_read 0
> > >
> > > This is not intentionally rejected, right?
> >
> > The way you wrote it, with goto +3, yes, it's intentional. Note that
> > you'll get different results in privileged and unprivileged modes.
> > Privileged mode allows "bounded loops" logic, so it doesn't
> > immediately reject this program, and then later sees that r8 is always
> > < 0x64, so program is correct.
> >
>
> I load the program with privileged mode, and goto-5 makes the program
> run from #9 to #5, so r8 is updated and the program is not infinite loop.
>
> > But in unprivileged mode the rules are different, and this conditional
> > back edge is not allowed, which is probably what you are getting.
> >
> > It's actually confusing and your "back-edge from insn 7 to 8" is out
> > of date and doesn't correspond to your program, you should see
> > "back-edge from insn 11 to 7", please double check.
> >
>
> Yes it's also confusing to me, but "back-edge from insn 7 to 8" is what
> I got. The execution path of the program is #4 to #8 (goto+3), so the
> verifier see the #8 first. Then, the program then goes #9 to #5 (goto-5),
> the verifier thus sees #7 to #8 and incorrectly concludes back-edge here.
>
> This can is the verifier log I got from latest bpf-next, this C program can
> reproduce this: https://pastebin.com/raw/Yug0NVwx
Your instruction indices in your comments are wrong. Save yourself
time and confusion, use embedded assembly and llvm-objdump. You also
have a mismatch between 0x64 and actually specifying 0x68. Anyways, I
don't know how you got 7 to 8, but there does seem indeed to be a bug
in check_cfg() falsely detecting this as an infinite loop even in
privileged mode, which it should. I'll need to look deeper into how to
fix check_cfg(), it's not the easier to follow code, unfortunately.
But here's my log for your information.
$ git show
commit a343e644b8f3757a83f48b32b56ffc83943a62fa (HEAD -> temp-back-edge-test)
Author: Andrii Nakryiko <[email protected]>
Date: Thu Nov 2 11:55:11 2023 -0700
selftests/bpf: trickier case of "bounded loop"
This should be accepted in privileged mode because r8 = 2 * r4 = 0x6a,
and so `if r8 < 0x64 goto -5;` is always false. Currently BPF verifier's
check_cfg() doesn't detect this properly.
Reported-by: Hao Sun <[email protected]>
Signed-off-by: Andrii Nakryiko <[email protected]>
diff --git a/tools/testing/selftests/bpf/progs/verifier_cfg.c
b/tools/testing/selftests/bpf/progs/verifier_cfg.c
index df7697b94007..f89dce7850f6 100644
--- a/tools/testing/selftests/bpf/progs/verifier_cfg.c
+++ b/tools/testing/selftests/bpf/progs/verifier_cfg.c
@@ -97,4 +97,26 @@ l0_%=: r2 = r0;
\
" ::: __clobber_all);
}
+SEC("socket")
+__description("conditional loop (2)")
+__success
+__failure_unpriv __msg_unpriv("back-edge from insn 10 to 11")
+__naked void conditional_loop2(void)
+{
+ asm volatile (" \
+ r9 = 2 ll; \
+ r3 = 0x20 ll; \
+ r4 = 0x35 ll; \
+ r8 = r4; \
+ goto l1_%=; \
+l0_%=: r9 -= r3; \
+ r9 -= r4; \
+ r9 -= r8; \
+l1_%=: r8 += r4; \
+ if r8 < 0x64 goto l0_%=; \
+ r0 = r9; \
+ exit; \
+" ::: __clobber_all);
+}
+
char _license[] SEC("license") = "GPL";
Here's disassembly (though I moved it to separate .bpf.c file to have
0-based instruction indices, my patch above adds test to other
existing tests):
$ llvm-objdump -d verifier_cfg1.bpf.o
verifier_cfg1.bpf.o: file format elf64-bpf
Disassembly of section socket:
0000000000000000 <conditional_loop2>:
0: 18 09 00 00 02 00 00 00 00 00 00 00 00 00 00 00 r9 = 0x2 ll
2: 18 03 00 00 20 00 00 00 00 00 00 00 00 00 00 00 r3 = 0x20 ll
4: 18 04 00 00 35 00 00 00 00 00 00 00 00 00 00 00 r4 = 0x35 ll
6: bf 48 00 00 00 00 00 00 r8 = r4
7: 05 00 03 00 00 00 00 00 goto +0x3 <l1_0>
0000000000000040 <l0_0>:
8: 1f 39 00 00 00 00 00 00 r9 -= r3
9: 1f 49 00 00 00 00 00 00 r9 -= r4
10: 1f 89 00 00 00 00 00 00 r9 -= r8
0000000000000058 <l1_0>:
11: 0f 48 00 00 00 00 00 00 r8 += r4
12: a5 08 fb ff 64 00 00 00 if r8 < 0x64 goto -0x5 <l0_0>
13: bf 90 00 00 00 00 00 00 r0 = r9
14: 95 00 00 00 00 00 00 00 exit
Then running test on latest bpf-next:
$ sudo ./test_progs -t verifier_cfg
...
run_subtest:PASS:obj_open_mem 0 nsec
libbpf: prog 'conditional_loop2': BPF program load failed: Invalid argument
libbpf: prog 'conditional_loop2': failed to load: -22
libbpf: failed to load object 'verifier_cfg'
run_subtest:FAIL:unexpected_load_failure unexpected error: -22 (errno 22)
VERIFIER LOG:
=============
10: asm volatile (" \
back-edge from insn 10 to 11
processed 0 insns (limit 1000000) max_states_per_insn 0 total_states 0
peak_states 0 mark_read 0
=============
#329/15 verifier_cfg/conditional loop (2):FAIL
#329/16 verifier_cfg/conditional loop (2) @unpriv:OK
#329 verifier_cfg:FAIL
I'll keep looking into this after taking care of other stuff I have on
TODO list, thanks.
>
> > Anyways, while I was looking into this, I realized that ldimm64 isn't
> > handled exactly correctly in check_cfg(), so I just sent a fix. It
> > also adds a nicer detection of jumping into the middle of the ldimm64
> > instruction, which I believe is something you were advocating for.
> >
> > >
> > > Best
> > > Hao