linux-kernel - Re: [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives
Hash Suite: Windows password security audit tool. GUI, reports in PDF.
[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Message-ID: <CACkBjsauBbmKRAgEhOujtpGBeAWksar9yS+0hk1i9pLYwtQN3A@mail.gmail.com>
Date: Mon, 17 Nov 2025 11:30:04 +0100
From: Hao Sun <sunhao.th@...il.com>
To: Alexei Starovoitov <alexei.starovoitov@...il.com>
Cc: bpf <bpf@...r.kernel.org>, Alexei Starovoitov <ast@...nel.org>, 
	Daniel Borkmann <daniel@...earbox.net>, Andrii Nakryiko <andrii@...nel.org>, Eduard <eddyz87@...il.com>, 
	John Fastabend <john.fastabend@...il.com>, Martin KaFai Lau <martin.lau@...ux.dev>, 
	Song Liu <song@...nel.org>, Yonghong Song <yonghong.song@...ux.dev>, 
	LKML <linux-kernel@...r.kernel.org>, Hao Sun <hao.sun@....ethz.ch>
Subject: Re: [PATCH RFC 00/17] bpf: Introduce proof-based verifier enhancement

On Sat, Nov 15, 2025 at 3:27 AM Alexei Starovoitov
<alexei.starovoitov@...il.com> wrote:
>
> I tried to categorize failures from many of these ~1500
> and lots of them are similar.
>
> In paper you mention 3 examples:
> - ptr + str_pos, with size MAX - str_pos
> - s>>= 31
> - &= 0xffff
>
> Did you categorize all 1500 failures into categories?
>
> What are the specific gaps in the verifier beyond these 3 cases ?

There are additional patterns beyond the three cases mentioned
earlier. I reviewed
several other object files and their verifier logs, and in some
instances, the root
are insufficient tracking of relationships between registers.

The example below was analyzed manually by me. Let me know if you spot
any mistakes.

clang-15_-O1_felix_bin_bpf_from_wep_debug_v6.o/calico_tc_skb_accepted_entrypoint:
```
...
572: (61) r1 = *(u32 *)(r10 -272)     ;
R1=scalar(id=70,smin=smin32=0,smax=umax=smax32=umax32=0xffff,var_off=(0x0;
0xffff))
573: (54) w1 &= 255                   ;
R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff))
574: (bc) w2 = w1                     ;
R1=scalar(id=233,smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff)) R2=scalar(id=233,smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff))
575: (04) w2 += -4                    ;
R2=scalar(smin=0,smax=umax=0xffffffff,smin32=-4,smax32=251,var_off=(0x0;
0xffffffff))
576: (a6) if w2 < 0x2 goto pc+130     ;
R2=scalar(smin=umin=umin32=2,smax=umax=0xffffffff,smin32=-4,smax32=251,var_off=(0x0;
0xffffffff))
577: (56) if w1 != 0x0 goto pc+8      ; R1=0
578: (61) r1 = *(u32 *)(r8 +432)
...
R3 !read_ok
```
>From 576 to 577, (w1&255) + -4 >= 2, so w1&255 >= 6; hence, 577 to 578
is unreachable.

clang-19_-O1_seccomp_x86_bpfel.o/ig_seccomp_e:
```
30: (79) r8 = *(u64 *)(r7 +8)         ; R7=ctx() R8=scalar()
...
41: (bf) r1 = r8                      ; R1=scalar(id=2) R8=scalar(id=2)
42: (67) r1 <<= 32                    ;
R1=scalar(smax=0x7fffffff00000000,umax=0xffffffff00000000,smin32=0,smax32=umax32=0,var_off=(0x0;
0xffffffff00000000))
43: (77) r1 >>= 32                    ;
R1=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
44: (25) if r1 > 0x1f3 goto pc+98     ;
R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=499,var_off=(0x0;
0x1ff))
45: (bf) r1 = r10                     ; R1=fp0 R10=fp0
...
139: (57) r8 &= 511                   ;
R8=scalar(smin=smin32=0,smax=umax=smax32=umax32=511,var_off=(0x0;
0x1ff))
140: (0f) r0 += r8                    ;
R0=map_value(map=syscalls_per_mn,ks=8,vs=501,smin=smin32=0,smax=umax=smax32=umax32=511,var_off=(0x0;
0x1ff)) R8=scalar(smin=smin32=0,smax=umax=smax32=umax32=511,var_off=(0x0;
0x1ff))
141: (b7) r1 = 1                      ; R1=1
142: (73) *(u8 *)(r0 +0) = r1
invalid access to map value, value_size=501 off=511 size=1
```
>From 44 to 45, r1<=499; hence, w8<=499 After r8&=511, the access is safe.
The above cases are hard to address with small improvements to the verifier.

I did find lots of similar cases where the imprecision causes were similar.
This is limited by the way we reveal those false rejections (i.e., compile
the same source with different compiler configurations).

clang-17_-O1_felix_bin_bpf_to_l3_debug.o/calico_tc_host_ct_conflict:
```
1899: (63) *(u32 *)(r10 -296) = r8    ;
R8=scalar(id=56,smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff))
1900: (16) if w8 == 0x6 goto pc+1     ;
R8=scalar(id=56,smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff))
1901: (b7) r3 = 0                     ; R3=0
1902: (61) r6 = *(u32 *)(r10 -216)    ; R6=0 R10=fp0 fp-216=????0
1903: (61) r1 = *(u32 *)(r10 -296)    ;
R1=scalar(id=56,smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff)) R10=fp0 fp-296=????scalar(id=56,smin=smin32=0,smax=umax=smax32=umax32=255,var_off=(0x0;
0xff))
...
1907: (56) if w1 != 0x6 goto pc+10    ; R1=6
1908: (69) r1 = *(u16 *)(r3 +12)
R3 invalid mem access 'scalar'
```
The fact w8!=6 (from 1900 to 1901) is not 'remembered', the unreachable path
(from 1907 to 1908) is mistakenly taken. One possible fix is another
state forking
on the neq path to remember this information and propagate this information to
all the regs and slots that share the same ID. But again, this leads more states
to explore on neq/eq branches.

Another case that is trivially the same:
clang-15_-O1_felix_bin_bpf_from_hep_dsr_no_log_co-re.o/calico_tc_skb_accepted_entrypoint:
```
262: (56) if w8 != 0x5 goto pc+4 267: R3=scalar(id=171,...)
R8=scalar(id=171,var_off=(0x0; 0xff))
267: (56) if w8 != 0x5 goto pc+16     ; R8=5
268: (61) r4 = *(u32 *)(r7 +372)      ; unreachable
269: (61) r3 = *(u32 *)(r1 +0)
R1 invalid mem access 'scalar'
```