Tracing input values and running symbolic execution

[vinatgit]

Hi I am trying to reverse engineer a binary that is available to me (which stores my input at some location and then checks that with a hardcoded string, and returns the output accordingly). I want to know if there is a functionality in Miasm that allows me to trace my input, run symbolic execution and solve the above mentioned problem.

[commial]

Hi,

You may want to take a look at the DSE module (miasm2.analysis.dse) which runs a symbolic execution alongside a concrete one. If I correctly understand your problem, you can:

1. runs your code with a Miasm jitter
2. attach a DSE instance once you've entered your input
3. symbolize your input (with apply_change or symbolize_memory)

Then, you can either:

• Ask for the equation of the final returning value (which will then depends on your symbolic input)
• Override some DSE methods to catch path condition on your input (when IRDst becomes symbolic, it means that it depends on your input, the rest being only concrete).

A blog post is on its way for this plug-in, it might be clearer :)