Wednesday, May 8, 2013
The capability of using SMT solvers to solve and reduce equations makes me wonder if it would be possible to generate and solve equations generated by analyzing x86 asm instructions. Each basic block were taken an equation could be generated with the RHS as the value being compared against just before the jump of a basic block(an oversimplification I agree, I doubt that this will have any practical implications at all!). This is mainly meant to be used on a parsed tracelog rather than the disassembly/binary as such. I have a very basic PoC uploaded here that uses the Python API for the z3 SMT solver, I'll keep uploading newer gists as revisions.