vbpf / prevail / 30246333287

87%

push

github

Fix 32-bit soundness holes that let unsafe programs pass verification

Two independent classes of ALU32/JMP32 unsoundness allowed a crafted program to
be accepted while performing an out-of-bounds stack access.

MOVSX: the no-op fast path returned early for `wX sN= wX`, skipping the
zero-extension applied at the end of the function. The verifier kept a
sign-extended 64-bit value where the CPU produces a zero-extended 32-bit one, so
`r1 = r10; r2 = -1; w2 s8= r2; r1 += r2` was analyzed as r10 - 1 while the CPU
computes r10 + 0xFFFFFFFF, and the resulting out-of-bounds store was proved
in-bounds. The verifier already contradicted itself here: with r1 = -1,
`w2 s8= r1` yielded 0xFFFFFFFF but `w2 s8= r2` yielded -1 for the same operation
and input. Guard the fast path with bin.is64; the 64-bit form remains a no-op.

32-bit compares: the helpers emitted constraints over the 64-bit svalue/uvalue
variables after testing only the truncated 32-bit views. When a register's
64-bit value falls outside the 32-bit range those views say nothing about how the
64-bit variables are ordered, so branches that concrete executions do take were
proved dead, and unsafe code on them was never checked. Test the 64-bit intervals
instead, falling back to the existing no-constraint case. Precision is unchanged
for registers holding genuine 32-bit values, since the comparison itself pins the
operand's sign in the branches that assert one.

assume_unsigned_32bit_lt already guarded every branch this way, which is why only
the >, >=, s<, s<=, s> and s>= paths were affected.

Also drop the interval parameters these helpers no longer read.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

19 of 19 new or added lines in 2 files covered. (100.0%)

9328 of 10751 relevant lines covered (86.76%)

6280627.17 hits per line