symMMU: symbolically executed runtime libraries for symbolic memory access.

ABSTRACTSymbolic execution calls for specialized address translation. Unlike a pointer on a traditional machine model, which corresponds to a single address, a symbolic pointer may represent multiple feasible addresses. A symbolic pointer dereference manipulates symbolic state, potentially submitting many theorem prover requests in the process. Hence, design and management of symbolic accesses critically affects symbolic executor performance, complexity, and completeness. We demonstrate a symbolic execution extension, the symMMU, which separates access dispatch mechanism from policy by servicing memory accesses with symbolically executed runtime software handlers. This runtime code concisely represents access policies including pointer concretization, address forking, and symbolic indexing. These policies are competitive with a baseline hard-coded memory policy. Furthermore, the symMMU cleanly supports handlers for profiling, heap analysis, and demand allocated symbolic buffers. In practice, the symMMU flags hardware-validated bugs for over a thousand Linux program binaries.