Audit symbolic pointer concretization

Symbolic execution is only as complete as its memory and environment models. A pointer can be symbolic in the solver while a memory operation quietly chooses one concrete address, discarding behavior that the analyst expected to remain symbolic.

Research anchor and scope

angr’s symbolic memory documentation describes ordered read/write concretization strategies. Its documented default writes include bounded handling for annotated multiwrites and a fallback choosing the maximum possible address. It offers SYMBOLIC_WRITE_ADDRESSES and range strategies to change that behavior. The page was reviewed on October 12, 2026; inspect the installed angr version’s strategy objects rather than treating the documentation’s defaults as a timeless API guarantee.

Make the lost path visible

Suppose a toy binary takes an index constrained to {0,1} and writes a byte into buffer[index]. Later it succeeds only if buffer[0] changed. A model that resolves the write to index 1 can miss the success path even though index 0 satisfies the input constraints. “No solution found” now describes the modeled execution, not the original program’s full behavior.

Before changing settings, record the symbolic expression, its possible range, and constraints added during address resolution. Use address-concretization inspection points to see what the engine selected. Compare this with the addresses that the real binary can use for the same input domain.

Choose a bounded model

Constrain genuine pointer domains where justified by the binary: array bounds, alignment, base addresses, and allocation ranges. A small set of candidate addresses can be represented with conditional stores; a nearly unconstrained 64-bit pointer is far more expensive. Increasing the range limit indiscriminately may replace a missing-path problem with memory exhaustion.

If several regions are possible, split states by region or index and document the split. A manually fixed pointer can help analyze one path but must be labeled as an assumption. Verify that hooks and SimProcedures preserve side effects relevant to the success condition; a perfect memory strategy cannot compensate for an external function modeled as returning arbitrary success.

Validate solver results concretely

Replay candidate inputs against the real binary or a faithful local harness. Check both output and side effects. An input that satisfies a simplified success address may fail due to initialization, file access, calling convention, or pointer aliasing omitted from the state.

Also test a deliberately constructed expected path to ensure the model can reach it. This catches overconstraint and concretization losses before expensive exploration. Maintain a model ledger with concretized memory operations, unmodeled environment effects, and justified constraints. Symbolic execution should narrow the analysis while preserving an explicit account of what has been approximated; neither a satisfying model nor an empty search is automatically a complete proof about the executable.