Abstract-block mode fired one over-approximate onBinaryArith per block with
fresh unconstrained operands, so it proved nothing for div-by-zero / null-deref
(0 binary findings on libdiv_by_zero / libnull_deref). A full per-instruction
symbolic encoder with path modeling is the eventual fix, but on symbolic args
an unconstrained overflow/aliasing check is trivially SAT and would fire on
every add/sub/mul (the FP blowup) — so this slice lands the sound, zero-FP
subset: constant-zero propagation.
scanInstructionsForConstHazards (pure, unit-tested): a per-function state
machine tracking which registers / stack slots provably hold 0.
mov r,0 | mov r,wzr | str wzr,[slot] | ldr r,[zeroed-slot] -> r/slot is 0
sdiv/udiv d,a,b with b==0 -> div by zero
ldr/str through a zero base register [x0] -> null deref
Tracking resets at every branch / call / ret, so it never reasons across an
unmodeled path — no false positives, at the cost of missing path-dependent
zeros (div_by_zero_variable, null_deref_conditional remain FN: those need
branch modeling, deferred).
Both structural disasm passes (this + UAF) now share one per-function pdfj
sweep via disasmFindingsInSession; const-hazard scanning runs default-on
alongside the import/string detectors and under --detectors
security/div-by-zero/null-deref. Findings carry Heuristic confidence.
Validated on the CTF corpus: +3 TP — div_by_zero_direct, mod_by_zero
(CWE-369), null_deref_direct (CWE-476), all previously FN in binary mode —
with zero new findings across the other 8 dylibs. 6 r2-free unit tests
(test_binary_const_hazards) cover literal-zero divisor, slot-propagated null
deref, non-zero/unknown divisors, branch-reset, and non-zero pointer
negatives. 70 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
