You are now the owner of this repo.

vbpf / prevail
87%

DEFAULT BRANCH: main
Repo Added
Token ENVZUPw7kXSVTNwI0SnEWS5mIrwoBd6UH regen
Build 948 Last
Files 79
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

LAST BUILD ON BRANCH main
branch: SELECT
CHANGE BRANCH
x
Sync Branches

coverage: 86.764% (+0.002%) from 86.762%
30246333287

push

github

elazarg 
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 0 new or added lines in 0 files covered. (NaN%)

28 existing lines in 2 files now uncovered.

9328 of 10751 relevant lines covered (86.76%)

6280627.17 hits per line

Relevant lines Covered
10751 RELEVANT LINES 9328 COVERED LINES
6280627.17 HITS PER LINE
Source Files on main

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
30246333287 main 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... push elazarg github
86.76
30220794353 fix/alu32-soundness Merge 126250114 into b4ebed601 Pull #1214 GitHub github
86.76
30096987245 main Handle out-of-bounds negative stack offset without crashing (fixes #1211) (#1212) A stack access at a negative constant offset (a stack pointer walked below its frame) crashed the verifier with an uncaught InternalError instead of rejecting the o... push web-flow github
86.76
30049892521 feat/linear-relation-domain Merge 31c474d22 into 07558f088 Pull #1213 GitHub github
87.1
29851398100 main Reconstruct inlined callee's internal edges in a second pass (fixes #1203) (#1209) * Reconstruct inlined callee's internal edges in a second pass (fixes #1203) When a bpf-to-bpf local function is inlined, `add_cfg_nodes` reconstructed the clone'... push web-flow github
86.76
29851285864 main Reset per-SCC vertex marks in select_potentials (fixes #1201) (#1210) `select_potentials` runs Bellman-Ford per SCC to assign valid potentials during meet, using `vert_marks` to track which vertices belong to the SCC currently being processed (BF... push web-flow github
86.76
29850994034 fix/stack-offset-narrow-crash Merge e705f9c07 into b8dd92616 Pull #1212 web-flow github
86.76
29784313676 fix/stack-offset-narrow-crash Merge 9b3da880a into b8dd92616 Pull #1212 web-flow github
86.76
29783290643 fix/stack-offset-narrow-crash Merge 994a9dd86 into b8dd92616 Pull #1212 web-flow github
86.76
29781093587 fix/1203-inlined-callee-backedge Merge 86e0bf212 into b8dd92616 Pull #1209 web-flow github
86.76
See All Builds (925)

Badge your Repo: prevail

We detected this repo isn’t badged! Grab the embed code to the right, add it to your repo to show off your code coverage, and when the badge is live hit the refresh button to remove this message.
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

Refresh