Re: [bpf PATCH] bpf: verifier, do_refine_retval_range may clamp umin to 0 incorrectly

[Yonghong Song <yhs@fb.com>]

On 1/24/20 12:36 AM, Daniel Borkmann wrote:
> On 1/24/20 8:10 AM, John Fastabend wrote:
>> do_refine_retval_range() is called to refine return values from specified
>> helpers, probe_read_str and get_stack at the moment, the reasoning is
>> because both have a max value as part of their input arguments and
>> because the helper ensure the return value will not be larger than this
>> we can set umax and smax values of the return register, r0.
>>
>> However, the return value is a signed integer so setting umax is 
>> incorrect
>> It leads to further confusion when the do_refine_retval_range() then 
>> calls,
>> __reg_deduce_bounds() which will see a umax value as meaning the value is
>> unsigned and then assuming it is unsigned set the smin = umin which in 
>> this
>> case results in 'smin = 0' and an 'smax = X' where X is the input 
>> argument
>> from the helper call.
>>
>> Here are the comments from _reg_deduce_bounds() on why this would be safe
>> to do.
>>
>>   /* Learn sign from unsigned bounds.  Signed bounds cross the sign
>>    * boundary, so we must be careful.
>>    */
>>   if ((s64)reg->umax_value >= 0) {
>>     /* Positive.  We can't learn anything from the smin, but smax
>>      * is positive, hence safe.
>>      */
>>     reg->smin_value = reg->umin_value;
>>     reg->smax_value = reg->umax_value = min_t(u64, reg->smax_value,
>>                           reg->umax_value);
>>
>> But now we incorrectly have a return value with type int with the
>> signed bounds (0,X). Suppose the return value is negative, which is
>> possible the we have the verifier and reality out of sync. Among other
>> things this may result in any error handling code being falsely detected
>> as dead-code and removed. For instance the example below shows using
>> bpf_probe_read_str() causes the error path to be identified as dead
>> code and removed.
>>
>>> From the 'llvm-object -S' dump,
>>
>>   r2 = 100
>>   call 45
>>   if r0 s< 0 goto +4
>>   r4 = *(u32 *)(r7 + 0)
>>
>> But from dump xlate
>>
>>    (b7) r2 = 100
>>    (85) call bpf_probe_read_compat_str#-96768
>>    (61) r4 = *(u32 *)(r7 +0)  <-- dropped if goto
>>
>> Due to verifier state after call being
>>
>>   R0=inv(id=0,umax_value=100,var_off=(0x0; 0x7f))
>>
>> To fix omit setting the umax value because its not safe. The only
>> actual bounds we know is the smax. This results in the correct bounds
>> (SMIN, X) where X is the max length from the helper. After this the
>> new verifier state looks like the following after call 45.
>>
>> R0=inv(id=0,smax_value=100)
>>
>> Then xlated version no longer removed dead code giving the expected
>> result,
>>
>>    (b7) r2 = 100
>>    (85) call bpf_probe_read_compat_str#-96768
>>    (c5) if r0 s< 0x0 goto pc+4
>>    (61) r4 = *(u32 *)(r7 +0)
>>
>> Note, bpf_probe_read_* calls are root only so we wont hit this case
>> with non-root bpf users.
>>
>> Fixes: 849fa50662fbc ("bpf: verifier, refine bounds may clamp umin to 
>> 0 incorrectly")
>> Signed-off-by: John Fastabend <john.fastabend@gmail.com>
> 
> Been reviewing this fix internally, therefore also:
> 
> Reviewed-by: Daniel Borkmann <daniel@iogearbox.net>
> 
> Still waiting to give Yonghong a chance to take a look as well before 
> applying
> and getting bpf PR out (should be roughly in morning US time).

The change makes sense to me. Thanks!
Acked-by: Yonghong Song <yhs@fb.com>