Skip to content

Remove narrowing conversion to satisfy verifier#5

Merged
DispatchCode merged 8 commits intoDispatchCode:mainfrom
work-robot:main
Mar 5, 2026
Merged

Remove narrowing conversion to satisfy verifier#5
DispatchCode merged 8 commits intoDispatchCode:mainfrom
work-robot:main

Conversation

@work-robot
Copy link
Contributor

@work-robot work-robot commented Mar 3, 2026

This is actually quite interesting: narrowing u64 -> u32 confuses the verifier:

; index += stats->head;
142: (79) r4 = *(u64 *)(r0 +384)      ; R0=map_value(off=0,ks=4,vs=400,imm=0) R4_w=scalar() # r4 is unbounded because stats->head is unbounded
143: (bf) r5 = r2                     ; R2=15 R5_w=15 # r2 is the iterator, and due to loop unrolling, we know it's exactly 15
144: (0f) r5 += r4                    ; R4_w=scalar() R5_w=scalar() # r4 is unbounded => r5 is unbounded
145: (bf) r6 = r5                     ; R5_w=scalar(id=4) R6_w=scalar(id=4)
# narrow r6 before comparison with MAX_USER_PF_ENTRIES, since "index" is u32
146: (67) r6 <<= 32                   ; R6_w=scalar(smax=9223372032559808512,umax=18446744069414584320,var_off=(0x0; 0xffffffff00000000),s32_min=0,s32_max=0,u32_max=0)
147: (77) r6 >>= 32                   ; R6_w=scalar(umax=4294967295,var_off=(0x0; 0xffffffff))
# speculate the branch where we do index -= MAX_USER_PF_ENTRIES;
148: (bf) r4 = r5                     ; R4_w=scalar(id=4) R5_w=scalar(id=4)
149: (07) r4 += -16                   ; R4_w=scalar() # r4 is still unbounded, because the verifier doesn't know that stats->head stays within [0, 16)
; if (index >= MAX_USER_PF_ENTRIES) {
# skip over r4 = r5 if r6 is small enough
150: (25) if r6 > 0xf goto pc+1       ; R6_w=scalar(umax=15,var_off=(0x0; 0xf))
# this would reset r4 to r5, instead of r4 == r5-16
151: (bf) r4 = r5                     ; R4_w=scalar(id=4) R5_w=scalar(id=4)
# commit either r5 or r5-16 to r5; note the verifier doesn't know r5 <= 16 since it doesn't know stats->head <= 16
152: (bf) r5 = r4                     ; R4_w=scalar(id=4) R5_w=scalar(id=4) # at this point, r5 and r4 are still identical
153: (67) r5 <<= 32                   ; R5_w=scalar(smax=9223372032559808512,umax=18446744069414584320,var_off=(0x0; 0xffffffff00000000),s32_min=0,s32_max=0,u32_max=0)
154: (77) r5 >>= 32                   ; R5_w=scalar(umax=4294967295,var_off=(0x0; 0xffffffff))
# at this point, r5 != r4 because we've narrowed r5 but the verifier doesn't understand narrowing
; if (stat) {
155: (25) if r5 > 0xf goto pc-27      ; R5_w=scalar(umax=15,var_off=(0x0; 0xf)) # we've checked r5, but not r4, since it's unlinked from r5 due to the narrowing! r4 is still unbounded!
; if (index < MAX_USER_PF_ENTRIES) {
# narrow r4 because the iterator is u32
156: (67) r4 <<= 32                   ; R4_w=scalar(smax=9223372032559808512,umax=18446744069414584320,var_off=(0x0; 0xffffffff00000000),s32_min=0,s32_max=0,u32_max
=0)
157: (77) r4 >>= 32                   ; R4_w=scalar(umax=4294967295,var_off=(0x0; 0xffffffff))
158: (27) r4 *= 24                    ; R4_w=scalar(umax=103079215080,var_off=(0x0; 0x1ffffffff8),s32_max=2147483640,u32_max=-8)
159: (bf) r5 = r0                     ; R0=map_value(off=0,ks=4,vs=400,imm=0) R5_w=map_value(off=0,ks=4,vs=400,imm=0)
160: (0f) r5 += r4                    ; R4_w=scalar(umax=103079215080,var_off=(0x0; 0x1ffffffff8),s32_max=2147483640,u32_max=-8) R5_w=map_value(off=0,ks=4,vs=400,umax=103079215080,var_off=(0x0; 0x1ffffffff8),s32_max=2147483640,u32_max=-8)
; event->pf[i].cr2 = stat->cr2;
161: (79) r4 = *(u64 *)(r5 +0)
R5 unbounded memory access, make sure to bounds check any such access
processed 550 insns (limit 1000000) max_states_per_insn 3 total_states 18 peak_states 18 mark_read 5
-- END PROG LOAD LOG --

work-robot and others added 8 commits March 2, 2026 19:16
Pull request creation failed. Validation failed: must be a collaborator
The BPF verifier deals poorly with narrowing conversions u32 -> u64,
which are implemented by clang as (r <<= 32; r >>= 32;). This breaks
register identities and hence bounds checks on "identical" registers.
The test mostly checks that the BPF program can be loaded and reports
reasonable addresses for the page faults. It also checks the cr2 field
from signal_generate.
@DispatchCode DispatchCode merged commit e707891 into DispatchCode:main Mar 5, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants