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

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

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