Alan-Jowett / ebpf-verifier
87%

DEFAULT BRANCH: main
Repo Added
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

coverage: 86.764% (+0.1%) from 86.649%
30559636792

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 19 new or added lines in 2 files covered. (100.0%)

107 existing lines in 5 files now uncovered.

9328 of 10751 relevant lines covered (86.76%)

6280124.66 hits per line

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

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
30559636792 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
29279923487 main Drive sample verification tests from the inventory; parallelize CI (#1195) Full-program verification of the ebpf-samples corpus was 17 C++ files generated by scripts/generate_verify_project_tests.py from test-data/elf_inventory.json, then compile... push web-flow github
86.65
28137986881 main Bump actions/checkout from 6 to 7 Bumps [actions/checkout](https://github.com/actions/checkout) from 6 to 7. - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)... push elazarg github
86.39
27778108035 main Release v0.2.5 Bump project version to 0.2.5 and add a CHANGELOG entry covering ELF loader hardening, numeric-domain soundness fixes, and the writable helper output initialization documentation update since v0.2.4. Also updates the using_installe... push elazarg github
86.39
24597451955 dependabot/github_actions/softprops/action-gh-release-3 Merge f9467a679 into b9010eee4 Pull #177 web-flow github
88.98
23971858946 dependabot/submodules/external/libbtf-6a09e51 Merge 8edcac58e into b9010eee4 Pull #176 web-flow github
88.98
23971858138 dependabot/submodules/external/bpf_conformance-f558566 Merge 79078ef91 into b9010eee4 Pull #175 web-flow github
88.98
23372535569 dependabot/submodules/external/libbtf-0570bf0 Merge b6d9862d0 into b9010eee4 Pull #173 web-flow github
88.98
23372536310 dependabot/submodules/external/bpf_conformance-15e0553 Merge d9b74c65c into b9010eee4 Pull #174 web-flow github
88.98
23080970838 dependabot/submodules/external/bpf_conformance-8e6ed4a Merge 60d05c8d9 into b9010eee4 Pull #171 web-flow github
88.98
See All Builds (321)