Re: [PATCH bpf-next v2 1/2] bpf: Track aligned st store as imprecise spilled registers

[Yonghong Song <yonghong.song@linux.dev>]

On 1/8/24 12:05 PM, Eduard Zingerman wrote:
> On Mon, 2024-01-08 at 11:51 -0800, Yonghong Song wrote:
> [...]
>>> In case if check_stack_read_var_off() would be modified to check not
>>> only for STACK_ZERO, but also for zero spills, I think that all such
>>> spills would have to be marked precise at the time of read,
>>> as backtracking would not be able to find those later.
>> I don't understand the above. If the code pattern looks like
>>     r1 = ...; /* r1 range [-32, -16);
>>     *(u8 *)(r10 + r1) = r2;
>>     ...
>>     r3 = *(u8 *)(r10 + r1);
>>     r3 needs to be marked as precise.
>>
>> Conservatively marking r2 in '*(u8 *)(r10 + r1) = r2' as precise
>> should be the correct way to do.
>>
>> Or you are thinking even more complex code pattern like
>>     *(u64 *)(r10 - 32) = r4;
>>     *(u64 *)(r10 - 24) = r5;
>>     ...
>>     r1 = ...; /* r1 range [-32, -16) */
>>     r3 = *(u8 *)(r10 + r1);
>>     r3 needs to be marked as precise.
>>
>> In this case, we should proactively mark r4 and r5 as precise.
>> But currently we did not do it, right?
> Yes, I'm thinking about the latter scenario.
> There would be zero spills for fp-32 and fp-24.
> If check_stack_read_var_off() is modified to handle zero spills,
> then it would conclude that r3 is zero.
> But if r3 is later marked precise, there would be no info for
> backtracking to mark fp-32, fp-24, r4, r5 as precise:
> - either backtracking info would have to be supplemented with a list
>    of stack locations that were spilled zeros at time of
>    check_stack_read_var_off();
> - or check_stack_read_var_off() would need to conservatively mark
>    all spilled zeros as precise.
>
> Nothing like that is needed now, because check_stack_read_var_off()
> would return unbound scalar for r3 upon seeing zero spill.
>
>> I think this later case is a very unlikely case.
> But it is possible and verifier has to be conservative.

Indeed. Such variable stack read has been handled properly.

Now I think I understand better on how verifier works for
load/store with var offsets. Basically some small changes
in check_stack_write_var_off(). Will post v3 soon.