Home
SENinja is a plugin for the disassembler BinaryNinja. The plugin implements a symbolic executor for the LLIL language of BinaryNinja, heavily inspired by angr and Ponce.
It currently supports x86, x86_64 and ARMv7, but can be extended easily with new architectures (see Extend).
Install z3 using pip: pip3 install z3-solver.
Clone the repository in the plugin folder of binary ninja, or install it using the plugin manager.
To use the plugin, open a binary for a supported architecture (currently x86, x86_64 and ARMv7), select an instruction, open the the right click menu and select Start Symbolic Execution. The command will create and initialize the first state, i.e., the object that stores the memory, the register values and the constraints during the execution. The instruction at which the state is going to execute is highlighted in green.
In this page we will use the embedded python console to interact with the plugin. See Widgets to have a look at our UI widgets that simplifies common operations.
The initial state will be initialized using the memory layout of the binary and using the Value Set Analysis performed by binary ninja. All the memory locations and registers whose value is unknown will be initialized with symbols (this behavior can be changed in the settings).
You can use the embedded python console to interact with the state (look at this page to view the documentation of the python APIs):
import borzacchiello_seninja as seninja
s = seninja.get_current_state()
rax_value = s.regs.rax # get value of rax
s.regs.rax = seninja.BVS("symb", 64) # set the value of rax to the symbol "symb"
s.regs.rax = seninja.BVV(0xdeadbeef, 64) # set the value of rax to the concrete value 0xdeadbeef
m = s.mem.load(0x1000, 2) # get from memory two bytes at address 0x1000 (big endian by default)
m = s.mem.load(0x1000, 2, 'little') # the same, but little endian
s.mem.store(0x1000, rax_value) # store at address 0x1000 the bitvector rax_value
[...]Now we are able to interact with the state, but we are not executing any instruction. In SENinja there is always one active state that is executing. There are a few ways to execute instructions, all of them are accessible through the right-click menu:
- Step: it is the most basic command, which processes one instruction.
- Continue until branch: it will execute instructions until a symbolic branch is reached, i.e., until a new state is generated.
- Continue until address: instructions will be executed until the currently selected address is reached. At branches, if a new state is generated, only one state is selected as the current state. So, beware because this command could not terminate if the address is never reached or if the current state remains stuck in a loop. This command should be used if we want to reach an address and we are sure that it will be reached (e.g., a long basic block).
- Run (DFS or BFS): to use this command, an address must be selected as the target of the search (using the right-click menu). It will execute instructions using a DFS or BFS algorithm to find the searched address. The DFS algorithm is more efficient but can remain stuck in loops.
Note that all these commands can generate new states. These new states are highlighted in red in the CFG, and the current state can be changed with a queued state using the right-click menu (change current state).
We executed instructions on the state, now what? We can use the solver to solve the formulas that we built during the excution! Every state has a solver that owns the path constraint of the state, i.e., its condition of validity. To interact with the solver, we can use the embedded python console:
s = seninja.get_current_state()
# evaluate the value of register rax, and get bytes
s.solver.evaluate(s.regs.rax).as_bytes()
# evaluate the value of register rbx, with the additional constraint that rax==42
s.solver.evaluate(s.regs.rbx, [s.regs.rax == 42]).as_bytes()
# evaluate the value of register, giving up to 10 solutions
s.solver.evaluate_upto(s.regs.rcx, 10)
# add the constraint that the byte at address 0x1000 must be equal to the char 'a'
s.solver.add_constraint(s.mem.load(0x1000, 1) == ord('a'))
[...]Dynamically linked functions and system calls are handled using models (just like angr). The models simulates the behavior of the function (or syscall), modifying accordingly the current state. Currently, the plugin supports some models, but new models can be added easily (see Extend).
To overcome the lack of a model, or to perform a specific operation when the execution reaches an address, the user can define custom hooks:
def hook(state):
state.regs.rax = seninja.BVV(0, 64)
return state, [], [] # new_state, new_deferred, new_errored
seninja.register_hook(0x401300, hook)this code will call the function hook when the execution reaches the address 0x401300. The hook function just set the value of the register rax to zero.