Skip to content

v0.2.0

Pre-release
Pre-release

Choose a tag to compare

View all tags
@elazarg elazarg released this 22 Feb 20:45
· 176 commits to main since this release
v0.2.0
a69e70a
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Prevail v0.2.0

This release brings a major expansion to Prevail's type system, platform modeling, and safety guarantees, along with significant performance improvements and a much friendlier user experience. (33 commits since v0.1.3).

Major Highlights

Equational & Non-Convex Type Domain

The type domain has been completely overhauled: it is now equational and non-convex (no longer relying on the Zone domain for types). This fundamental change allows the verifier to precisely track unrelated types simultaneously, significantly improving analysis accuracy and reducing false positives.

Expanded Type System

  • New Type Encodings: Added support for T_SOCKET, T_BTF_ID, T_ALLOC_MEM, and T_FUNC, with full propagation through helper calls and return values.
  • Callback Validation: Callback targets (e.g., bpf_for_each_map_elem, bpf_timer_set_callback) are now type-checked to be valid function entry points. Callback body verification is not yet implemented.
  • Allocation Tracking: Allocation size bounds are now tracked and verified for functions like ringbuf_reserve.
  • Tail Calls: Tail call chain depth is now bounded and parity-checked.

Advanced Platform Modeling

  • 200+ Helpers: Linux platform tables expanded to over 200 helpers with full, per-helper ABI type signatures (replacing the previous 6 generic groups).
  • kfunc Support: Added table-driven kfunc (CALL src=2) resolution and validation.
  • Context Descriptors: Updated context struct sizes and descriptors for over 30 program types against kernel 6.14 headers (tracing, struct_ops, lsm, lirc_mode2, syscall, netfilter, etc.).
  • Builtins: Standard builtin calls (memset, memcpy, memmove, memcmp) are now resolved and accurately modeled.
  • Instruction Lowering: Added LDDW pseudo-address lowering.

ELF Loader Rewrite

The monolithic ELF loader has been completely rewritten into a modular src/io/ package. It now features separate, robust components for map parsing, CO-RE relocations, and extern resolution. Malformed ELF inputs are now caught and reported gracefully instead of throwing unhandled exceptions.

Diagnostics & UX Improvements

  • Failure Slicing: New --failure-slice flag prints a minimal causal trace from a verification error back to its root cause, filtering out irrelevant instructions.
  • Human-Friendly Output: Replaced the legacy CSV output format with readable PASS: section/function / FAIL: section/function messages, including the first error encountered and a helpful hint.
  • Quiet Mode: Added -q/--quiet to suppress stdout and only return an exit code.

Performance

  • >4x Faster: Verification on large programs is over 4x faster thanks to deep optimizations in both the numeric and new type domains.

Safe and Sound (Bug Fixes)

This release resolves several critical safety-soundness bugs to ensure strict verification:

  • Fixed a stale shared_region_size issue after ambiguous map lookups that could allow Out-Of-Bounds (OOB) reads.
  • Fixed stale caller-saved registers after subprogram returns that could allow Use-After-Free (UAF).
  • Fixed 32-bit signed/unsigned comparison intervals that previously ignored bitwidth (#874, #875).
  • Fixed a bug where mismatched helper context types were accepted without a check (#192).
  • Fixed an assertion crash in Assume when operands had different types (#1012).
  • Fixed incorrect context descriptor sizes across 12 program types (#959).
  • Fixed widening instability in the zone domain that caused non-termination loops (#960).
  • Fixed 8 packet-modifying helpers that were missing the reallocate_packet flag.
  • Strictly reject null pointer dereferences with non-zero access sizes.

Breaking Changes

  • Executable Renamed: The main binary is now bin/prevail.
  • CLI Options Removed: The --domain option has been removed (zoneCrab is now implicit, and legacy dead-code paths for linux/stats were dropped).
  • Output Format: Standard CSV output ({0|1},{seconds},{memory_kb}) has been completely replaced by the new human-readable format. Scripts relying on the old format will need to be updated.

Infrastructure & Testing

  • The test suite has been massively expanded to 1525 cases covering real-world ELF binaries.
  • Test expectations are now managed via a machine-readable JSON inventory (elf_inventory.json), generating per-project test files automatically.
Assets 5
Loading