Re: [PATCH bpf-next 2/3] bpf: infer packet range for 'if pkt ==/!= pkt_end' comparisons

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

On 1/8/24 5:28 AM, Eduard Zingerman wrote:
> Extend try_match_pkt_pointers() to handle == and != operations.
> For instruction:
>
>        .--------------- pointer to packet with some range R
>        |     .--------- pointer to packet end
>        v     v
>    if rA == rB goto ...
>
> It is valid to infer that R bytes are available in packet.
> This change should allow verification of BPF generated for
> C code like below:
>
>    if (data + 42 != data_end) { ... }
>
> Suggested-by: Maciej Żenczykowski <zenczykowski@gmail.com>
> Link: https://lore.kernel.org/bpf/CAHo-Oow5V2u4ZYvzuR8NmJmFDPNYp0pQDJX66rZqUjFHvhx82A@mail.gmail.com/
> Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
> ---
>   kernel/bpf/verifier.c | 8 ++++++++
>   1 file changed, 8 insertions(+)
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index 918e6a7912e2..b229ba0ad114 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -14677,6 +14677,7 @@ static bool try_match_pkt_pointers(const struct bpf_insn *insn,
>   				   struct bpf_verifier_state *this_branch,
>   				   struct bpf_verifier_state *other_branch)
>   {
> +	struct bpf_verifier_state *eq_branch;
>   	int opcode = BPF_OP(insn->code);
>   	int dst_regno = insn->dst_reg;
>   
> @@ -14713,6 +14714,13 @@ static bool try_match_pkt_pointers(const struct bpf_insn *insn,
>   		find_good_pkt_pointers(other_branch, dst_reg, dst_reg->type, opcode == BPF_JLT);
>   		mark_pkt_end(this_branch, dst_regno, opcode == BPF_JLE);
>   		break;
> +	case BPF_JEQ:
> +	case BPF_JNE:
> +		/* pkt_data ==/!= pkt_end, pkt_meta ==/!= pkt_data */
> +		eq_branch = opcode == BPF_JEQ ? other_branch : this_branch;
> +		find_good_pkt_pointers(eq_branch, dst_reg, dst_reg->type, true);
> +		mark_pkt_end(eq_branch, dst_regno, false);
> +		break;

What will happen if there are multiple BPF_JEQ/BPF_JNE? I made a change to one of tests
in patch 3:

+SEC("tc")
+__success __log_level(2)
+__msg("if r3 != r2 goto pc+3         ; R2_w=pkt_end() R3_w=pkt(off=8,r=0xffffffffffffffff)")
+__naked void data_plus_const_neq_pkt_end(void)
+{
+       asm volatile ("                                 \
+       r9 = r1;                                        \
+       r1 = *(u32*)(r9 + %[__sk_buff_data]);           \
+       r2 = *(u32*)(r9 + %[__sk_buff_data_end]);       \
+       r3 = r1;                                        \
+       r3 += 8;                                        \
+       if r3 != r2 goto 1f;                            \
+       r3 += 8;                                        \
+       if r3 != r2 goto 1f;                            \
+       r1 = *(u64 *)(r1 + 0);                          \
+1:                                                     \
+       r0 = 0;                                         \
+       exit;                                           \
+"      :
+       : __imm_const(__sk_buff_data, offsetof(struct __sk_buff, data)),
+         __imm_const(__sk_buff_data_end, offsetof(struct __sk_buff, data_end))
+       : __clobber_all);
+}


The verifier output:
func#0 @0
Global function data_plus_const_neq_pkt_end() doesn't return scalar. Only those are supported.
0: R1=ctx() R10=fp0
; asm volatile ("                                       \
0: (bf) r9 = r1                       ; R1=ctx() R9_w=ctx()
1: (61) r1 = *(u32 *)(r9 +76)         ; R1_w=pkt(r=0) R9_w=ctx()
2: (61) r2 = *(u32 *)(r9 +80)         ; R2_w=pkt_end() R9_w=ctx()
3: (bf) r3 = r1                       ; R1_w=pkt(r=0) R3_w=pkt(r=0)
4: (07) r3 += 8                       ; R3_w=pkt(off=8,r=0)
5: (5d) if r3 != r2 goto pc+3         ; R2_w=pkt_end() R3_w=pkt(off=8,r=0xffffffffffffffff)
6: (07) r3 += 8                       ; R3_w=pkt(off=16,r=0xffffffffffffffff)
7: (5d) if r3 != r2 goto pc+1         ; R2_w=pkt_end() R3_w=pkt(off=16,r=0xffffffffffffffff)
8: (79) r1 = *(u64 *)(r1 +0)          ; R1=scalar()
9: (b7) r0 = 0                        ; R0_w=0
10: (95) exit

from 7 to 9: safe

from 5 to 9: safe
processed 13 insns (limit 1000000) max_states_per_insn 0 total_states 1 peak_states 1 mark_read 0

insn 5, for this_branch (straight one), r3 range will be 8 and assuming pkt_end is 8.
insn 7, r3 range becomes 18 and then we assume pkt_end is 16.

I guess we should handle this case. For branch 5 and 7, it cannot be that both will be true.

>   	default:
>   		return false;
>   	}