vbpf / prevail / 28867867633

87%

push

github

Havoc the stack per-type for a multi-typed PTR_TO_WRITABLE_MEM argument (#1176)

The PTR_TO_WRITABLE_MEM helper-argument case computed the target address with
the no-type primary_kind_variable_for_type(param.mem) and bailed when it
returned nullopt -- which happens whenever the register's type is not a
singleton. But the checker only requires mem in {stack, packet, shared} plus a
write ValidAccess; it does not require a singleton type. So a register whose
abstract type is e.g. {stack, shared} passes the check, reaches the transformer,
hits the nullopt bail, and the stack region the helper may overwrite is never
havoced -- its stale known values persist, and a later load can read a stale
value and validate an operation that is unsafe at runtime (a false accept).

Mirror the sibling PTR_TO_WRITABLE_LONG/INT case: compute the stack address
per type inside join_over_types via primary_kind_variable_for_type(param.mem,
type) and havoc (and store_numbers) in the T_STACK branch, so the stack is
havoced for the T_STACK possibility even when the type is not a singleton.

Verified by structural correspondence to the already-correct WRITABLE_LONG/INT
path and by no regression across the [yaml] transformer tests and the full
non-slow [samples] suite. A discriminating end-to-end test was not added: the
triggering scenario (a multi-typed writable-mem pointer with a known stack cell)
is not reachable through the YAML/helper harness, consistent with the issue's
own medium-confidence assessment of end-to-end exploitability.

Guard store_numbers on "mem is definitely stack" (as the original code did via
its store_numbers flag) while keeping the per-type havoc that fixes the
stale-value leak. No regression across [yaml] and the full non-slow [samples]
suite.

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

10 of 12 new or added lines in 1 file covered. (83.33%)

9149 of 10575 relevant lines covered (86.52%)

6471832.38 hits per line