vbpf / prevail
87%

DEFAULT BRANCH: main
Repo Added
Token ENVZUPw7kXSVTNwI0SnEWS5mIrwoBd6UH regen
Build 945 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.762%. Remained the same
30096987245

push

github

web-flow 
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 out-of-bounds access:

    CRAB ERROR: Number -8 does not fit into m; function narrow, line 208

The strong-update path narrows the byte offset to the unsigned cell-offset type
Index (uint64_t): `n->narrow<Index>()` in both `kill_and_find_var` (used by
havoc/havoc_type/store/store_type) and `split_number_var`. A negative singleton
offset does not fit an unsigned type, so narrow throws and aborts the whole
analysis -- a robustness/DoS hole on adversarial input.

Guard the constant-offset path with `n->fits<Index>()`, exactly the condition
under which the narrow is safe. A negative offset has no corresponding stack
cell, so the cell bookkeeping is skipped and the out-of-bounds access is left
for the assertion checker to reject. Verified end-to-end that the crash becomes
a clean rejection ("Lower bound must be at least
r10.stack_offset - subprogram_stack_size") rather than a silent accept.

Regression test in test_array_domain.cpp drives store_type/havoc_type/havoc/
store with a negative singleton offset and asserts no throw and that the
in-bounds cell is untouched; it throws the InternalError without the fix.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QRunjNUunuZjp6KiBSZXzt
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

* Don't route negative constant stack offsets through symbolic kill (

Addresses review feedback. The guard only prevented the narrow
crash: a negative singleton offset left `res` empty and fell through to the
symbolic kill path, which builds the inclusive range `ii | (ii + elem_size)`
(e.g. [-8, 0]). That range overlaps the tracked cell [0, 8) at the shared
endpoint 0, so a havoc/store at a negative offset erased th... (continued)

9326 of 10749 relevant lines covered (86.76%)

6319078.39 hits per line

Relevant lines Covered
10749 RELEVANT LINES 9326 COVERED LINES
6319078.39 HITS PER LINE
Source Files on main

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
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
29779616095 fix/1201-select-potentials-spurious-bottom Merge 32baba502 into b8dd92616 Pull #1210 web-flow github
86.76
29778242089 main Havoc exact-match stack cell on kill (fixes #1202) `get_overlap_cells` deliberately excludes the exact-match cell (o, size) because loads handle it separately via `get_cell`. But `kill_and_find_var` reuses `get_overlap_cells` for the havoc path, ... push elazarg github
86.76
See All Builds (923)

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