* [RFC PATCH bpf-next] verifier: fix computation of range for XOR
@ 2024-04-05 22:08 Cupertino Miranda
2024-04-08 16:55 ` Yonghong Song
2024-04-08 17:47 ` Alexei Starovoitov
0 siblings, 2 replies; 6+ messages in thread
From: Cupertino Miranda @ 2024-04-05 22:08 UTC (permalink / raw)
To: bpf; +Cc: jose.marchesi, david.faust, elena.zannoni, Cupertino Miranda
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(-)
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
--
2.39.2
^ permalink raw reply related [flat|nested] 6+ messages in thread
* Re: [RFC PATCH bpf-next] verifier: fix computation of range for XOR
2024-04-05 22:08 [RFC PATCH bpf-next] verifier: fix computation of range for XOR Cupertino Miranda
@ 2024-04-08 16:55 ` Yonghong Song
2024-04-08 18:55 ` Cupertino Miranda
2024-04-08 17:47 ` Alexei Starovoitov
1 sibling, 1 reply; 6+ messages in thread
From: Yonghong Song @ 2024-04-08 16:55 UTC (permalink / raw)
To: Cupertino Miranda, bpf; +Cc: jose.marchesi, david.faust, elena.zannoni
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [RFC PATCH bpf-next] verifier: fix computation of range for XOR
2024-04-05 22:08 [RFC PATCH bpf-next] verifier: fix computation of range for XOR Cupertino Miranda
2024-04-08 16:55 ` Yonghong Song
@ 2024-04-08 17:47 ` Alexei Starovoitov
2024-04-08 20:02 ` Cupertino Miranda
1 sibling, 1 reply; 6+ messages in thread
From: Alexei Starovoitov @ 2024-04-08 17:47 UTC (permalink / raw)
To: Cupertino Miranda; +Cc: bpf, Jose E. Marchesi, David Faust, elena.zannoni
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [RFC PATCH bpf-next] verifier: fix computation of range for XOR
2024-04-08 16:55 ` Yonghong Song
@ 2024-04-08 18:55 ` Cupertino Miranda
0 siblings, 0 replies; 6+ messages in thread
From: Cupertino Miranda @ 2024-04-08 18:55 UTC (permalink / raw)
To: Yonghong Song; +Cc: bpf, jose.marchesi, david.faust, elena.zannoni
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [RFC PATCH bpf-next] verifier: fix computation of range for XOR
2024-04-08 17:47 ` Alexei Starovoitov
@ 2024-04-08 20:02 ` Cupertino Miranda
2024-04-08 20:06 ` Cupertino Miranda
0 siblings, 1 reply; 6+ messages in thread
From: Cupertino Miranda @ 2024-04-08 20:02 UTC (permalink / raw)
To: Alexei Starovoitov; +Cc: bpf, Jose E. Marchesi, David Faust, elena.zannoni
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [RFC PATCH bpf-next] verifier: fix computation of range for XOR
2024-04-08 20:02 ` Cupertino Miranda
@ 2024-04-08 20:06 ` Cupertino Miranda
0 siblings, 0 replies; 6+ messages in thread
From: Cupertino Miranda @ 2024-04-08 20:06 UTC (permalink / raw)
To: Alexei Starovoitov; +Cc: bpf, Jose E. Marchesi, David Faust, elena.zannoni
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2024-04-08 20:06 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-04-05 22:08 [RFC PATCH bpf-next] verifier: fix computation of range for XOR Cupertino Miranda
2024-04-08 16:55 ` Yonghong Song
2024-04-08 18:55 ` Cupertino Miranda
2024-04-08 17:47 ` Alexei Starovoitov
2024-04-08 20:02 ` Cupertino Miranda
2024-04-08 20:06 ` Cupertino Miranda
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.