Skip to content

Home

Jump to bottom
luca borzacchiello edited this page Sep 29, 2020 · 17 revisions

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.

How to install

TODO

How to use

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.

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 initilized with symbols (this behavior can be changed in the settings).

You can use the embedded python console to interact with the state:

import 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 remain 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).

Clone this wiki locally