Re: [RFC PATCH bpf-next] verifier: fix computation of range for XOR

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



Alexei Starovoitov writes:

> On Fri, Apr 5, 2024 at 3:08 PM Cupertino Miranda
> <cupertino.miranda@xxxxxxxxxx> 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.





[Index of Archives]     [Linux Samsung SoC]     [Linux Rockchip SoC]     [Linux Actions SoC]     [Linux for Synopsys ARC Processors]     [Linux NFS]     [Linux NILFS]     [Linux USB Devel]     [Video for Linux]     [Linux Audio Users]     [Yosemite News]     [Linux Kernel]     [Linux SCSI]


  Powered by Linux