| Message ID | 20240405220817.100451-1-cupertino.miranda@oracle.com (mailing list archive) |
|---|---|
| State | RFC |
| Delegated to: | BPF |
| Headers | show |
| Series | [RFC,bpf-next] verifier: fix computation of range for XOR | expand |
On 4/5/24 3:08 PM, Cupertino Miranda wrote: > Hi everyone, > > This email is a follow up on the problem identified in > https://github.com/systemd/systemd/issues/31888. > This problem first shown as a result of a GCC compilation for BPF that ends > converting a condition based decision tree, into a logic based one (making use > of XOR), in order to compute expected return value for the function. > > This issue was also reported in > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both > the original reproducer pattern and some other that also fails within clang. > > I have included a patch that contains a possible fix (I wonder) and a test case > that reproduces the issue in attach. > The execution of the test without the included fix results in: > > VERIFIER LOG: > ============= > Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. > 0: R1=ctx() R10=fp0 > ; asm volatile (" \ @ verifier_bounds.c:755 > 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() > 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) > 2: (b7) r1 = 0 ; R1_w=0 > 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 > 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 > 5: (07) r2 += -8 ; R2_w=fp-8 > 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) > 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) > 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm > 11: (b4) w1 = 0 ; R1_w=0 > 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) > 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) > 16: (79) r0 = *(u64 *)(r0 +8) > invalid access to map value, value_size=8 off=8 size=8 > R0 min value is outside of the allowed memory range > processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 > ============= > > The test collects a random number and shifts it right by 63 bits to reduce its > range to (0,1), which will then xor to compute the value of w1, checking > if the value is either 0 or 1 after. > By analysing the code and the ranges computations, one can easily deduce > that the result of the XOR is also within the range (0,1), however: > > 11: (b4) w1 = 0 ; R1_w=0 > 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > ^ > |___ No range is computed for R1 > > The verifier seems to act pessimistically and will only compute a range for > dst_reg, if the src_reg is a known value. > This happens in: > > -- verifier.c:13700 -- > if (!src_known && > opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) { > __mark_reg_unknown(env, dst_reg); > return 0; > } > > Is this really a requirement for XOR (and OR) ? Not really. The earlier verifier is a little bit conservative and it is not improved since we didn't hit an issue until now. > Unless I am missing some corner case and based on the logic presented in > tnum_xor (and even in tnum_or), it seems to me that it is safe to compute a new > range for both XOR (and OR) in case both operands are not known. Please send a formal patch to bpf-next. This way proper review can be done. > > Looking forward to your comments. > > Regards, > Cupertino > > --- > kernel/bpf/verifier.c | 3 +- > .../selftests/bpf/progs/verifier_bounds.c | 33 +++++++++++++++++++ > 2 files changed, 35 insertions(+), 1 deletion(-) > > diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c > index 1c34b91b9583..850a2950e740 100644 > --- a/kernel/bpf/verifier.c > +++ b/kernel/bpf/verifier.c > @@ -13698,7 +13698,8 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env, > } > > if (!src_known && > - opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) { > + opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND > + && opcode != BPF_XOR) { > __mark_reg_unknown(env, dst_reg); > return 0; > } There are some other operators as well, e.g. BPF_OR, could you also help take a look? > diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c > index 960998f16306..b0f9aa9203f6 100644 > --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c > +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c > @@ -745,6 +745,39 @@ l1_%=: r0 = 0; \ > : __clobber_all); > } > > +SEC("socket") > +__description("bounds check for reg32_0 = 0, reg32_1 = (0,1), reg32_1 xor reg32_2") > +__success __failure_unpriv > +__msg_unpriv("R0 min value is outside of the allowed memory range") > +__retval(0) > +__naked void reg32_0_reg32_xor_reg_01(void) > +{ > + asm volatile (" \ > + call %[bpf_get_prandom_u32]; \ > + r6 = r0; \ > + r1 = 0; \ > + *(u64*)(r10 - 8) = r1; \ > + r2 = r10; \ > + r2 += -8; \ > + r1 = %[map_hash_8b] ll; \ > + call %[bpf_map_lookup_elem]; \ > + if r0 != 0 goto l0_%=; \ > + exit; \ > +l0_%=: w1 = 0; \ > + r6 >>= 63; \ > + w1 ^= w6; \ > + if w1 == 0 goto l1_%=; \ > + if w1 == 1 goto l1_%=; \ > + r0 = *(u64*)(r0 + 8); \ > +l1_%=: r0 = 0; \ > + exit; \ > +" : > + : __imm(bpf_map_lookup_elem), > + __imm_addr(map_hash_8b), > + __imm(bpf_get_prandom_u32) > + : __clobber_all); > +} > + > SEC("socket") > __description("bounds check for reg = 2, reg xor 3") > __success __failure_unpriv
On Fri, Apr 5, 2024 at 3:08 PM Cupertino Miranda <cupertino.miranda@oracle.com> wrote: > > Hi everyone, > > This email is a follow up on the problem identified in > https://github.com/systemd/systemd/issues/31888. > This problem first shown as a result of a GCC compilation for BPF that ends > converting a condition based decision tree, into a logic based one (making use > of XOR), in order to compute expected return value for the function. > > This issue was also reported in > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both > the original reproducer pattern and some other that also fails within clang. > > I have included a patch that contains a possible fix (I wonder) and a test case > that reproduces the issue in attach. > The execution of the test without the included fix results in: > > VERIFIER LOG: > ============= > Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. > 0: R1=ctx() R10=fp0 > ; asm volatile (" \ @ verifier_bounds.c:755 > 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() > 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) > 2: (b7) r1 = 0 ; R1_w=0 > 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 > 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 > 5: (07) r2 += -8 ; R2_w=fp-8 > 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) > 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) > 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm > 11: (b4) w1 = 0 ; R1_w=0 > 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) > 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) > 16: (79) r0 = *(u64 *)(r0 +8) > invalid access to map value, value_size=8 off=8 size=8 > R0 min value is outside of the allowed memory range > processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 > ============= > > The test collects a random number and shifts it right by 63 bits to reduce its > range to (0,1), which will then xor to compute the value of w1, checking > if the value is either 0 or 1 after. > By analysing the code and the ranges computations, one can easily deduce > that the result of the XOR is also within the range (0,1), however: > > 11: (b4) w1 = 0 ; R1_w=0 > 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) > ^ > |___ No range is computed for R1 > I'm missing why gcc generates insn 11 and 13 ? The later checks can compare r6 directly, right? The bugzilla links are too long to read. > Is this really a requirement for XOR (and OR) ? As Yonghong said, no one had the use case to make the verifier smarter, so pls send an official patch.
Yonghong Song writes: > On 4/5/24 3:08 PM, Cupertino Miranda wrote: >> Hi everyone, >> >> This email is a follow up on the problem identified in >> https://github.com/systemd/systemd/issues/31888. >> This problem first shown as a result of a GCC compilation for BPF that ends >> converting a condition based decision tree, into a logic based one (making use >> of XOR), in order to compute expected return value for the function. >> >> This issue was also reported in >> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both >> the original reproducer pattern and some other that also fails within clang. >> >> I have included a patch that contains a possible fix (I wonder) and a test case >> that reproduces the issue in attach. >> The execution of the test without the included fix results in: >> >> VERIFIER LOG: >> ============= >> Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. >> 0: R1=ctx() R10=fp0 >> ; asm volatile (" \ @ verifier_bounds.c:755 >> 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() >> 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) >> 2: (b7) r1 = 0 ; R1_w=0 >> 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 >> 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 >> 5: (07) r2 += -8 ; R2_w=fp-8 >> 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) >> 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) >> 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm >> 11: (b4) w1 = 0 ; R1_w=0 >> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) >> 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) >> 16: (79) r0 = *(u64 *)(r0 +8) >> invalid access to map value, value_size=8 off=8 size=8 >> R0 min value is outside of the allowed memory range >> processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 >> ============= >> >> The test collects a random number and shifts it right by 63 bits to reduce its >> range to (0,1), which will then xor to compute the value of w1, checking >> if the value is either 0 or 1 after. >> By analysing the code and the ranges computations, one can easily deduce >> that the result of the XOR is also within the range (0,1), however: >> >> 11: (b4) w1 = 0 ; R1_w=0 >> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> ^ >> |___ No range is computed for R1 >> >> The verifier seems to act pessimistically and will only compute a range for >> dst_reg, if the src_reg is a known value. >> This happens in: >> >> -- verifier.c:13700 -- >> if (!src_known && >> opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) { >> __mark_reg_unknown(env, dst_reg); >> return 0; >> } >> >> Is this really a requirement for XOR (and OR) ? > > Not really. The earlier verifier is a little bit conservative > and it is not improved since we didn't hit an issue until now. > >> Unless I am missing some corner case and based on the logic presented in >> tnum_xor (and even in tnum_or), it seems to me that it is safe to compute a new >> range for both XOR (and OR) in case both operands are not known. > > Please send a formal patch to bpf-next. This way proper review can be done. > >> >> Looking forward to your comments. >> >> Regards, >> Cupertino >> >> --- >> kernel/bpf/verifier.c | 3 +- >> .../selftests/bpf/progs/verifier_bounds.c | 33 +++++++++++++++++++ >> 2 files changed, 35 insertions(+), 1 deletion(-) >> >> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c >> index 1c34b91b9583..850a2950e740 100644 >> --- a/kernel/bpf/verifier.c >> +++ b/kernel/bpf/verifier.c >> @@ -13698,7 +13698,8 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env, >> } >> if (!src_known && >> - opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) { >> + opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND >> + && opcode != BPF_XOR) { >> __mark_reg_unknown(env, dst_reg); >> return 0; >> } > > There are some other operators as well, e.g. BPF_OR, could you also help take a look? Sure, will try to identify any other cases and send a patch. Thanks ! > >> diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c >> index 960998f16306..b0f9aa9203f6 100644 >> --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c >> +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c >> @@ -745,6 +745,39 @@ l1_%=: r0 = 0; \ >> : __clobber_all); >> } >> +SEC("socket") >> +__description("bounds check for reg32_0 = 0, reg32_1 = (0,1), reg32_1 xor reg32_2") >> +__success __failure_unpriv >> +__msg_unpriv("R0 min value is outside of the allowed memory range") >> +__retval(0) >> +__naked void reg32_0_reg32_xor_reg_01(void) >> +{ >> + asm volatile (" \ >> + call %[bpf_get_prandom_u32]; \ >> + r6 = r0; \ >> + r1 = 0; \ >> + *(u64*)(r10 - 8) = r1; \ >> + r2 = r10; \ >> + r2 += -8; \ >> + r1 = %[map_hash_8b] ll; \ >> + call %[bpf_map_lookup_elem]; \ >> + if r0 != 0 goto l0_%=; \ >> + exit; \ >> +l0_%=: w1 = 0; \ >> + r6 >>= 63; \ >> + w1 ^= w6; \ >> + if w1 == 0 goto l1_%=; \ >> + if w1 == 1 goto l1_%=; \ >> + r0 = *(u64*)(r0 + 8); \ >> +l1_%=: r0 = 0; \ >> + exit; \ >> +" : >> + : __imm(bpf_map_lookup_elem), >> + __imm_addr(map_hash_8b), >> + __imm(bpf_get_prandom_u32) >> + : __clobber_all); >> +} >> + >> SEC("socket") >> __description("bounds check for reg = 2, reg xor 3") >> __success __failure_unpriv
Alexei Starovoitov writes: > On Fri, Apr 5, 2024 at 3:08 PM Cupertino Miranda > <cupertino.miranda@oracle.com> wrote: >> >> Hi everyone, >> >> This email is a follow up on the problem identified in >> https://github.com/systemd/systemd/issues/31888. >> This problem first shown as a result of a GCC compilation for BPF that ends >> converting a condition based decision tree, into a logic based one (making use >> of XOR), in order to compute expected return value for the function. >> >> This issue was also reported in >> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both >> the original reproducer pattern and some other that also fails within clang. >> >> I have included a patch that contains a possible fix (I wonder) and a test case >> that reproduces the issue in attach. >> The execution of the test without the included fix results in: >> >> VERIFIER LOG: >> ============= >> Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. >> 0: R1=ctx() R10=fp0 >> ; asm volatile (" \ @ verifier_bounds.c:755 >> 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() >> 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) >> 2: (b7) r1 = 0 ; R1_w=0 >> 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 >> 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 >> 5: (07) r2 += -8 ; R2_w=fp-8 >> 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) >> 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) >> 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm >> 11: (b4) w1 = 0 ; R1_w=0 >> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) >> 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) >> 16: (79) r0 = *(u64 *)(r0 +8) >> invalid access to map value, value_size=8 off=8 size=8 >> R0 min value is outside of the allowed memory range >> processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 >> ============= >> >> The test collects a random number and shifts it right by 63 bits to reduce its >> range to (0,1), which will then xor to compute the value of w1, checking >> if the value is either 0 or 1 after. >> By analysing the code and the ranges computations, one can easily deduce >> that the result of the XOR is also within the range (0,1), however: >> >> 11: (b4) w1 = 0 ; R1_w=0 >> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >> ^ >> |___ No range is computed for R1 >> > > I'm missing why gcc generates insn 11 and 13 ? > The later checks can compare r6 directly, right? > The bugzilla links are too long to read. The code above is just some inline assembly in my patch that reproduces the specific GCC issue in the verifier. If you want to see the code GCC produces you can check in the systemd github issue. Thanks, Cupertino > >> Is this really a requirement for XOR (and OR) ? > > As Yonghong said, no one had the use case to make the verifier smarter, > so pls send an official patch.
Cupertino Miranda writes: > Alexei Starovoitov writes: > >> On Fri, Apr 5, 2024 at 3:08 PM Cupertino Miranda >> <cupertino.miranda@oracle.com> wrote: >>> >>> Hi everyone, >>> >>> This email is a follow up on the problem identified in >>> https://github.com/systemd/systemd/issues/31888. >>> This problem first shown as a result of a GCC compilation for BPF that ends >>> converting a condition based decision tree, into a logic based one (making use >>> of XOR), in order to compute expected return value for the function. >>> >>> This issue was also reported in >>> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both >>> the original reproducer pattern and some other that also fails within clang. >>> >>> I have included a patch that contains a possible fix (I wonder) and a test case >>> that reproduces the issue in attach. >>> The execution of the test without the included fix results in: >>> >>> VERIFIER LOG: >>> ============= >>> Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. >>> 0: R1=ctx() R10=fp0 >>> ; asm volatile (" \ @ verifier_bounds.c:755 >>> 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() >>> 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) >>> 2: (b7) r1 = 0 ; R1_w=0 >>> 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 >>> 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 >>> 5: (07) r2 += -8 ; R2_w=fp-8 >>> 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) >>> 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) >>> 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm >>> 11: (b4) w1 = 0 ; R1_w=0 >>> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) >>> 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) >>> 16: (79) r0 = *(u64 *)(r0 +8) >>> invalid access to map value, value_size=8 off=8 size=8 >>> R0 min value is outside of the allowed memory range >>> processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 >>> ============= >>> >>> The test collects a random number and shifts it right by 63 bits to reduce its >>> range to (0,1), which will then xor to compute the value of w1, checking >>> if the value is either 0 or 1 after. >>> By analysing the code and the ranges computations, one can easily deduce >>> that the result of the XOR is also within the range (0,1), however: >>> >>> 11: (b4) w1 = 0 ; R1_w=0 >>> 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) >>> ^ >>> |___ No range is computed for R1 >>> >> >> I'm missing why gcc generates insn 11 and 13 ? >> The later checks can compare r6 directly, right? >> The bugzilla links are too long to read. > > The code above is just some inline assembly in my patch that reproduces > the specific GCC issue in the verifier. > If you want to see the code GCC produces you can check in the systemd > github issue. > > Thanks, > Cupertino > Here is the log of the verifier from the code that GCC emitted. Mär 26 23:57:12 H systemd[1]: 0: R1=ctx(off=0,imm=0) R10=fp0 Mär 26 23:57:12 H systemd[1]: 0: (61) r0 = *(u32 *)(r1 +40) ; R0_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) R1=ctx(off=0,imm=0) Mär 26 23:57:12 H systemd[1]: 1: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 Mär 26 23:57:12 H systemd[1]: 2: (18) r1 = 0xffff8ef68fd28400 ; R1_w=map_ptr(off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 4: (07) r2 += -4 ; R2_w=fp-4 Mär 26 23:57:12 H systemd[1]: 5: (63) *(u32 *)(r10 -4) = r0 ; R0_w=scalar(smin=0,smax=umax=4294967295,var_off=(0x0; 0xffffffff)) R10=fp0 fp-8=mmmm???? Mär 26 23:57:12 H systemd[1]: 6: (85) call bpf_map_lookup_elem#1 ; R0_w=map_value_or_null(id=1,off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 7: (18) r1 = 0xffffb290805b6000 ; R1_w=map_value(off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 9: (71) r3 = *(u8 *)(r1 +0) ; R1_w=map_value(off=0,ks=4,vs=1,imm=0) R3_w=1 Mär 26 23:57:12 H systemd[1]: 10: (bf) r2 = r0 ; R0_w=map_value_or_null(id=1,off=0,ks=4,vs=1,imm=0) R2_w=map_value_or_null(id=1,off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 11: (57) r3 &= 255 ; R3_w=1 Mär 26 23:57:12 H systemd[1]: 12: (b7) r0 = 1 ; R0_w=1 Mär 26 23:57:12 H systemd[1]: 13: (15) if r2 == 0x0 goto pc+1 ; R2_w=map_value(off=0,ks=4,vs=1,imm=0) Mär 26 23:57:12 H systemd[1]: 14: (b7) r0 = 0 ; R0=0 Mär 26 23:57:12 H systemd[1]: 15: (87) r3 = -r3 ; R3_w=scalar() Mär 26 23:57:12 H systemd[1]: 16: (77) r3 >>= 63 ; R3_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) Mär 26 23:57:12 H systemd[1]: 17: (ac) w0 ^= w3 ; R0_w=scalar() R3_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) Mär 26 23:57:12 H systemd[1]: 18: (57) r0 &= 255 ; R0_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) Mär 26 23:57:12 H systemd[1]: 19: (95) exit Mär 26 23:57:12 H systemd[1]: At program exit the register R0 has value (0x0; 0xff) should have been in (0x0; 0x3) Mär 26 23:57:12 H systemd[1]: processed 18 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 Mär 26 23:57:12 H systemd[1]: -- END PROG LOAD LOG -- > >> >>> Is this really a requirement for XOR (and OR) ? >> >> As Yonghong said, no one had the use case to make the verifier smarter, >> so pls send an official patch.
diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c index 1c34b91b9583..850a2950e740 100644 --- a/kernel/bpf/verifier.c +++ b/kernel/bpf/verifier.c @@ -13698,7 +13698,8 @@ static int adjust_scalar_min_max_vals(struct bpf_verifier_env *env, } if (!src_known && - opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) { + opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND + && opcode != BPF_XOR) { __mark_reg_unknown(env, dst_reg); return 0; } diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c index 960998f16306..b0f9aa9203f6 100644 --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c @@ -745,6 +745,39 @@ l1_%=: r0 = 0; \ : __clobber_all); } +SEC("socket") +__description("bounds check for reg32_0 = 0, reg32_1 = (0,1), reg32_1 xor reg32_2") +__success __failure_unpriv +__msg_unpriv("R0 min value is outside of the allowed memory range") +__retval(0) +__naked void reg32_0_reg32_xor_reg_01(void) +{ + asm volatile (" \ + call %[bpf_get_prandom_u32]; \ + r6 = r0; \ + r1 = 0; \ + *(u64*)(r10 - 8) = r1; \ + r2 = r10; \ + r2 += -8; \ + r1 = %[map_hash_8b] ll; \ + call %[bpf_map_lookup_elem]; \ + if r0 != 0 goto l0_%=; \ + exit; \ +l0_%=: w1 = 0; \ + r6 >>= 63; \ + w1 ^= w6; \ + if w1 == 0 goto l1_%=; \ + if w1 == 1 goto l1_%=; \ + r0 = *(u64*)(r0 + 8); \ +l1_%=: r0 = 0; \ + exit; \ +" : + : __imm(bpf_map_lookup_elem), + __imm_addr(map_hash_8b), + __imm(bpf_get_prandom_u32) + : __clobber_all); +} + SEC("socket") __description("bounds check for reg = 2, reg xor 3") __success __failure_unpriv
Hi everyone, This email is a follow up on the problem identified in https://github.com/systemd/systemd/issues/31888. This problem first shown as a result of a GCC compilation for BPF that ends converting a condition based decision tree, into a logic based one (making use of XOR), in order to compute expected return value for the function. This issue was also reported in https://gcc.gnu.org/bugzilla/show_bug.cgi?id=114523 and contains both the original reproducer pattern and some other that also fails within clang. I have included a patch that contains a possible fix (I wonder) and a test case that reproduces the issue in attach. The execution of the test without the included fix results in: VERIFIER LOG: ============= Global function reg32_0_reg32_xor_reg_01() doesn't return scalar. Only those are supported. 0: R1=ctx() R10=fp0 ; asm volatile (" \ @ verifier_bounds.c:755 0: (85) call bpf_get_prandom_u32#7 ; R0_w=scalar() 1: (bf) r6 = r0 ; R0_w=scalar(id=1) R6_w=scalar(id=1) 2: (b7) r1 = 0 ; R1_w=0 3: (7b) *(u64 *)(r10 -8) = r1 ; R1_w=0 R10=fp0 fp-8_w=0 4: (bf) r2 = r10 ; R2_w=fp0 R10=fp0 5: (07) r2 += -8 ; R2_w=fp-8 6: (18) r1 = 0xffff8e8ec3b99000 ; R1_w=map_ptr(map=map_hash_8b,ks=8,vs=8) 8: (85) call bpf_map_lookup_elem#1 ; R0=map_value_or_null(id=2,map=map_hash_8b,ks=8,vs=8) 9: (55) if r0 != 0x0 goto pc+1 11: R0=map_value(map=map_hash_8b,ks=8,vs=8) R6=scalar(id=1) R10=fp0 fp-8=mmmmmmmm 11: (b4) w1 = 0 ; R1_w=0 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) 14: (16) if w1 == 0x0 goto pc+2 ; R1_w=scalar(smin=0x8000000000000001,umin=umin32=1) 15: (16) if w1 == 0x1 goto pc+1 ; R1_w=scalar(smin=0x8000000000000002,umin=umin32=2) 16: (79) r0 = *(u64 *)(r0 +8) invalid access to map value, value_size=8 off=8 size=8 R0 min value is outside of the allowed memory range processed 16 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 1 ============= The test collects a random number and shifts it right by 63 bits to reduce its range to (0,1), which will then xor to compute the value of w1, checking if the value is either 0 or 1 after. By analysing the code and the ranges computations, one can easily deduce that the result of the XOR is also within the range (0,1), however: 11: (b4) w1 = 0 ; R1_w=0 12: (77) r6 >>= 63 ; R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) 13: (ac) w1 ^= w6 ; R1_w=scalar() R6_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=1,var_off=(0x0; 0x1)) ^ |___ No range is computed for R1 The verifier seems to act pessimistically and will only compute a range for dst_reg, if the src_reg is a known value. This happens in: -- verifier.c:13700 -- if (!src_known && opcode != BPF_ADD && opcode != BPF_SUB && opcode != BPF_AND) { __mark_reg_unknown(env, dst_reg); return 0; } Is this really a requirement for XOR (and OR) ? Unless I am missing some corner case and based on the logic presented in tnum_xor (and even in tnum_or), it seems to me that it is safe to compute a new range for both XOR (and OR) in case both operands are not known. Looking forward to your comments. Regards, Cupertino --- kernel/bpf/verifier.c | 3 +- .../selftests/bpf/progs/verifier_bounds.c | 33 +++++++++++++++++++ 2 files changed, 35 insertions(+), 1 deletion(-)