This is a small and incomplete symbolic execution engine for x64 assembly programs. It reads assembly code in AT&T syntax e.g. as obtained from "objdump -d". It then runs the code in an interpreter mode, interpolating any missing inputs (registers, memory) using symbols and recording all symbolic computation in an AST.
The AST can be dumped as yaml and pickle files and further examined.
- Extend the AST analysis capabilities (e.g. using graph-tool)
- Add a constraint solving engine, able to solve a symbolic trace AST given a set of boundary conditions.
- Extend the supported instruction set
- Fix some of the limitations
- The memory model is too trivial and plain wrong (using a dict for any address, without any overlapping for e.g. 32bit and 64bit accesses to the same/consecutive addresses)
- Unreasonable symbolic memory access: This is just indexed by the address expression, yielding a new symbol for the memory. Some sort of memory closure and history-tracking for symbolic accesses would be needed, in order to identify the correct data during the solver step.
- No symbolic jump capability: Jump conditions need to be non-symbolically computable
- Not all registers implemented (especially 16bit/8bit/high-byte access modes)
- Severely limited subset of x86 instruction set (only supports part of the "unholy" example)
- Many more... :D
A real alternative can be found at: http://triton.quarkslab.com/