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

[Cupertino Miranda <cupertino.miranda@oracle.com>]

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.