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.825% (+0.2%) from 86.644%
37071205739

push

github

web-flow 
Stop descending iteration when narrowing is stationary (#1243)

* Stop descending iteration when narrowing is stationary

Descending fixpoint iteration currently stops only when the loop-body
transfer result subsumes the current invariant. If narrowing returns an
abstract state that is lattice-equivalent to the current invariant while
the transfer result remains strictly more precise, the next iteration
starts from the same abstract state and repeats until the descending
iteration limit.

Compute the narrowed candidate before assigning it and stop when it
mutually subsumes the current invariant. Retain the candidate so any
canonicalized representation or auxiliary stack-cell metadata is
preserved. Strict refinements continue as before, and the existing
iteration limit is unchanged.

Add a deterministic Extrapolator unit test covering strict meet and type
refinements followed by stationary numeric narrowing. Add the 32-bit
countdown reproducer from #783 as an end-to-end YAML regression.

Part of #783.

Signed-off-by: Michael Agun <danielagun@microsoft.com>
Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

* Address stationary narrowing review feedback

Rely on the narrowing contract that the refined state is below the
current invariant, so only the reverse ordering is needed to detect a
stationary result.

Replace the finite countdown YAML case, which PREVAIL rejected as a
false positive, with a true-positive regression. The same countdown SCC
still reaches stationary narrowing, then the program enters an
unconditional self-loop and is genuinely nonterminating.

Part of #783.

Signed-off-by: Michael Agun <danielagun@microsoft.com>

6 of 6 new or added lines in 1 file covered. (100.0%)

42 existing lines in 2 files now uncovered.

9121 of 10505 relevant lines covered (86.83%)

3202971.97 hits per line

Relevant lines Covered
10505 RELEVANT LINES 9121 COVERED LINES
3202971.97 HITS PER LINE
Source Files on main

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
37071205739 main Stop descending iteration when narrowing is stationary (#1243) * Stop descending iteration when narrowing is stationary Descending fixpoint iteration currently stops only when the loop-body transfer result subsumes the current invariant. If narr... push web-flow github
86.83
35374770339 main Bump github/codeql-action from 4.37.9 to 4.38.0 Bumps [github/codeql-action](https://github.com/github/codeql-action) from 4.37.9 to 4.38.0. - [Release notes](https://github.com/github/codeql-action/releases) - [Changelog](https://github.com/gith... push elazarg github
86.64
32153585176 main Bump external/libbtf from `6a09e51` to `07af232` Bumps [external/libbtf](https://github.com/Alan-Jowett/libbtf) from `6a09e51` to `07af232`. - [Release notes](https://github.com/Alan-Jowett/libbtf/releases) - [Commits](https://github.com/Alan-Jow... push elazarg github
85.99
31421448145 main Bump github/codeql-action from 4.37.3 to 4.37.6 Bumps [github/codeql-action](https://github.com/github/codeql-action) from 4.37.3 to 4.37.6. - [Release notes](https://github.com/github/codeql-action/releases) - [Changelog](https://github.com/gith... push elazarg github
85.99
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
See All Builds (325)