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

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2024-01-04 at 12:12 -0800, Yonghong Song wrote:
[...]
> > > @@ -4613,11 +4613,28 @@ static int check_stack_write_var_off(struct bpf_verifier_env *env,
> > >   
> > >   	/* Variable offset writes destroy any spilled pointers in range. */
> > >   	for (i = min_off; i < max_off; i++) {
> > > +		struct bpf_reg_state *spill_reg;
> > >   		u8 new_type, *stype;
> > > -		int slot, spi;
> > > +		int slot, spi, j;
> > >   
> > >   		slot = -i - 1;
> > >   		spi = slot / BPF_REG_SIZE;
> > > +
> > > +		/* If writing_zero and the the spi slot contains a spill of value 0,
> > > +		 * maintain the spill type.
> > > +		 */
> > > +		if (writing_zero && !(i % BPF_REG_SIZE) && is_spilled_scalar_reg(&state->stack[spi])) {
> > Talked to Andrii today, and he noted that spilled reg should be marked
> > precise at this point.
> 
> Could you help explain why?
> 
> Looks we did not mark reg as precise with fixed offset as below:
> 
>          if (reg && !(off % BPF_REG_SIZE) && register_is_bounded(reg) && env->bpf_capable) {
>                  save_register_state(env, state, spi, reg, size);
>                  /* Break the relation on a narrowing spill. */
>                  if (fls64(reg->umax_value) > BITS_PER_BYTE * size)
>                          state->stack[spi].spilled_ptr.id = 0;
>          } else if (!reg && !(off % BPF_REG_SIZE) && is_bpf_st_mem(insn) &&
>                     insn->imm != 0 && env->bpf_capable) {
> 
> I probably missed something about precision tracking...

The discussed justification was that if verifier assumes something
about the value of scalar (in this case that it is 0) such scalar
should be marked precise (e.g. this is done for value_regno in
check_stack_write_var_off()).

This seemed logical at the time of discussion, however, I can't figure
a counter example at the moment. It appears that whatever are
assumptions in check_stack_write_var_off() if spill is used in the
precise context it would be marked eventually.
E.g. the following is correctly rejected:

SEC("raw_tp")
__log_level(2) __flag(BPF_F_TEST_STATE_FREQ)
__failure
__naked void var_stack_1(void)
{
	asm volatile (
		"call %[bpf_get_prandom_u32];"
		"r9 = 100500;"
		"if r0 > 42 goto +1;"
		"r9 = 0;"
		"*(u64 *)(r10 - 16) = r9;"
		"call %[bpf_get_prandom_u32];"
		"r0 &= 0xf;"
		"r1 = -1;"
		"r1 -= r0;"
		"r2 = r10;"
		"r2 += r1;"
		"r0 = 0;"
		"*(u8 *)(r2 + 0) = r0;"
		"r1 = %[two_byte_buf];"
		"r2 = *(u32 *)(r10 -16);"
		"r1 += r2;"
		"*(u8 *)(r1 + 0) = r2;" /* this should not be fine */
		"exit;"
	:
	: __imm_ptr(two_byte_buf),
	  __imm(bpf_get_prandom_u32)
	: __clobber_common);
}

So now I'm not sure :(
Sorry for too much noise.