Search code, repositories, users, issues, pull requests...

This is a binary ninja plugin that implements a symbolic execution engine based only on z3, highly inspired by the angr framework (https://angr.io/). The plugin is implemented as an emulator of LLIL instructions that builds and manipulates z3 formulas.

SENinja simulates a debugger: the execution is path driven, only one state is active and executes instructions. The other states, generated at branches, are saved in a deferred queue. At any time, the active state can be changed with a deferred one.

The Register View can be used to visualize the value of the registers of the active state. The value of a register can be modifyied by double-clicking on it. The right-click menu allows to:

The Memory View can be used to visualize the value of a portion of memory of the active state. By clicking on "monitor memory", the user can specify a memory address to monitor. The widget will show 512 bytes starting from that address. The memory view is splitted in two sections: an hexview and an ascii view. The hexview shows the hex value of each byte only if the byte is mapped and concrete. If the byte is unmapped, the characted _ is shown; if the byte is symbolic, the widget shows the character ..

More APIs can be executed through the python shell. For example, we can use the solver to prove a condition for the current state:

Leave a Comment