search

borzacchiello / seninja

symbolic execution plugin for binary ninja
BSD 2-Clause "Simplified" License
244 stars 22 forks source link

Mismatches in registers and register names prevent execution #3

Closed shinmai closed 3 years ago

shinmai commented 3 years ago

Apologies if it's me not understanding how to work with SENinja but unmodified, I cannot get it to work at all, regardless of architecture (granted I only tried 32 and 64 bit ELF and PE executables), even with simple test binaries.

Trying to start symbolic execution, the plugin throws an unhandled KeyError exception at sym_executor.py:107 KeyError: 'mmx0'. As I said, this happens regardless of arch or bit-width. Wrapping the register initialisation for loop with try, except: pass obviously gets rid of the error, and SENinja seems to initialise a state correctly.

However, trying to step even one instruction throws another error at registers.py:46, AttributeError: 'Regs' object has not attribute 'gsbase'. If the last "fix" was hacky, that was nothing compared to this, but adding if(k=="gsbase"): k="gs" at the top of the __getattribute__ function in registers.py again fixes the issue and allows SENinja to step and do its thing.

As sated, this might all be me misunderstanding how SENinja works and how to use it, and my duct-tape fixes definitely don't pass muster for a proper solution, but they did work for me and allowed me to do what I wanted, and the values I pulled from SENinja, as a result, worked in real-life, so they seemed to work in my case at least. ¯\ _(ツ)_/¯

This is on Windows in 2.1.2440-dev (personal license), latest plug-in version available from the plug-in manager, Python 3.8.6 and z3-solver 4.8.9.0.

borzacchiello commented 3 years ago

Hi! Thank you for using the tool. Are you using the master version of SENinja? If not, try pulling it from GitHub directly in the plugin folder of binary ninja. The v0.1 release is broken on the latest version of binary ninja.

shinmai commented 3 years ago

Ah, I was indeed using the version from Binja's Plugin Manager. I uninstalled the Plugin Manager version and cloned the repo in it's place, but the plug-in won't even enable anymore with the error Failed to import python plugin: community/borzacchiello_seninja: No module named 'seninja'.

I'm not in urgent need of the tool right now, but the only way I can seem to get SENinja to run on the latest dev branch Binja for now is by using v0.1 with the manual changes outlined above.

borzacchiello commented 3 years ago

Just rename the folder from borzacchiello_seninja to seninja. It should work! BTW the version in the plug-in manager got updated, so you can use that now :)