Binary mode had no UAF/double-free detection. In abstract-block mode the Z3
encoder gives every call argument a fresh, unconstrained constant, so an
aliasing check (freed_ptr == deref_ptr) is trivially SAT for unrelated
pointers — it would fire on every post-free deref. A Z3-proven aliasing UAF
is therefore not viable until per-instruction value flow lands.
Instead detect it structurally over r2 per-instruction disassembly, keyed on
the *stack slot* a heap pointer lives in (r2 names it, e.g. `[ptr]`/`[dest]`)
— a reliable identity within one function, no aliasing needed:
scanInstructionsForUaf (pure, unit-tested): a per-function state machine.
ldr <reg>,[slot] -> reg sources slot
bl free -> slot dangling (double free if already dangling)
bl <other> -> use-after-free if the freed slot's pointer is the arg
str <alloc>,[slot]-> slot revived (free+realloc+free is legitimate)
detectUseAfterFreeFromDisasm / uafFindingsInSession: r2 wrapper, run from
R2Backend::runDetectors on the shared session (no extra `aaa`), default-on
alongside the import/string detectors and under --detectors
security/use-after-free/double-free. Findings carry Heuristic confidence.
Cost is bounded: skip entirely when the binary imports no free/delete (instant
on the common case) and cap the per-function pdfj sweep at 4000 functions.
Validated on bench/corpora/ctf-challenges/libuaf_doublefree.dylib: +3 TP
(double_free_bug CWE-415, use_after_free_bug + use_global_after_free CWE-416 —
all previously FN in binary mode), zero new findings across the other 9 corpus
dylibs. 5 r2-free unit tests (test_binary_uaf) cover double-free, UAF,
clean-free, free+realloc+free, and cross-slot negatives. 69 Ok / 0 Fail /
1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
