Re: [PATCH bpf-next 1/2] bpf: fix nullness propagation for reg to reg comparisons

[Yonghong Song]

On 12/11/22 8:09 PM, Hao Sun wrote:
> After befae75856ab, the verifier would propagate null information after
> JEQ/JNE, e.g., if two pointers, one is maybe_null and the other is not,
> the former would be marked as non-null in eq path. However, as comment
> "PTR_TO_BTF_ID points to a kernel struct that does not need to be null
> checked by the BPF program ... The verifier must keep this in mind and
> can make no assumptions about null or non-null when doing branch ...".
> If one pointer is maybe_null and the other is PTR_TO_BTF_ID, the former
> is incorrectly marked non-null. The following BPF prog can trigger a
> null-ptr-deref, also see this report for more details[1]:
>
> 	0: (18) r1 = map_fd	        ; R1_w=map_ptr(ks=4, vs=4)
> 	2: (79) r6 = *(u64 *)(r1 +8)    ; R6_w=bpf_map->inner_map_data
> 					; R6 is PTR_TO_BTF_ID
> 					; equals to null at runtime
> 	3: (bf) r2 = r10
> 	4: (07) r2 += -4
> 	5: (62) *(u32 *)(r2 +0) = 0
> 	6: (85) call bpf_map_lookup_elem#1    ; R0_w=map_value_or_null
> 	7: (1d) if r6 == r0 goto pc+1
> 	8: (95) exit
> 	; from 7 to 9: R0=map_value R6=ptr_bpf_map
> 	9: (61) r0 = *(u32 *)(r0 +0)          ; null-ptr-deref
> 	10: (95) exit
>
> So, make the verifier propagate nullness information for reg to reg
> comparisons only if neither reg is PTR_TO_BTF_ID.
>
> [1] https://lore.kernel.org/bpf/CACkBjsaFJwjC5oiw-1KXvcazywodwXo4zGYsRHwbr2gSG9WcSw@xxxxxxxxxxxxxx/T/#u
>
> Fixes: befae75856ab4 ("bpf: propagate nullness information for reg to reg comparisons")
> Signed-off-by: Hao Sun <sunhao.th@xxxxxxxxx>

Ack with a small nit below.

Acked-by: Yonghong Song <yhs@xxxxxx>

> ---
>   kernel/bpf/verifier.c | 4 +++-
>   1 file changed, 3 insertions(+), 1 deletion(-)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index a5255a0dcbb6..aa651e4517e0 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -11825,7 +11825,9 @@ static int check_cond_jmp_op(struct bpf_verifier_env *env,
>   	 */

Could you add explanation why PTR_TO_BTF_ID reg type should be excluded
in the above comments?

>   	if (!is_jmp32 && BPF_SRC(insn->code) == BPF_X &&
>   	    __is_pointer_value(false, src_reg) && __is_pointer_value(false, dst_reg) &&
> -	    type_may_be_null(src_reg->type) != type_may_be_null(dst_reg->type)) {
> +	    type_may_be_null(src_reg->type) != type_may_be_null(dst_reg->type) &&
> +	    base_type(src_reg->type) != PTR_TO_BTF_ID &&
> +	    base_type(dst_reg->type) != PTR_TO_BTF_ID) {
>   		eq_branch_regs = NULL;
>   		switch (opcode) {
>   		case BPF_JEQ: