Repository navigation
Python APIs
Many functionalities of SENinja can be accessed through the embedded python console of BinaryNinja.
It is also possible to write a .py script that uses the SENinja APIs and that can be executed using the embedded python console using this plugin.
This page provides some example of interaction with the SENinja APIs.
In this section we will see how to start the SENinja exploration without using the UI:
import seninja
seninja.start_se(bv, 0x4006c0) # Start the symbolic exploration at address 0x4006c0
seninja.setup_argv( # Setup ARGV for the current function (0x4006c0 is the address of the main function)
seninja.str_to_bv(str(16), terminator=True))
t, f = seninja.continue_until_branch() # Run the exploration until a branch, and returns the **true** (t) and **false** (f) states.
seninja.change_current_state(f.get_ip()) # Change the current state with the state `f`
s = seninja.continue_until_address(0x400700) # Run the exploration until the address 0x400700 for the current state.
seninja.reset_se() # Reset the explorationThe user can define custom hooks/loggers that will be executed when a state reaches an address. The difference between a logger and a hook is that the logger does not modify the state and executes the instruction, while the hook modifies the state and skip the instruction.
def hook(state):
state.regs.rax = seninja.BVV(0, 64)
return state, [], [] # new_state, new_deferred, new_errored
def logger(state):
print("State @ %#x [rax = %s]" % (state.get_ip(), state.regs.rax))
seninja.register_hook(0x401300, hook)
seninja.register_logger(0x401304, logger)this code will call the function hook when the execution reaches the address 0x401300. The hook function just sets the value of the register rax to zero.
In this section, we will see how to create and manipulate concrete bitvectors and symbolic expressions.
The code that implements expressions lives the /expr subfolder and is highly inspired by claripy.
import seninja # If you installed the plugin using the plugin manager,
# use `import borzacchiello_seninja as seninja`
concrete_bv = seninja.BVV(0xdeadbeef, 32) # value, size
concrete_bv += 10
concrete_bv *= 14
concrete_bv = concrete_bv.ZeroExt(32)
print(concrete_bv) # <BVV64 0x000000002d80719e>
print(concrete_bv.Extract(7, 0)) # <BVV8 0x9e>
print(concrete_bv.value) # 763392414
print(concrete_bv.as_bytes()) # b'\x00\x00\x00\x00-\x80q\x9e'
symbolic_bv = seninja.BVS("symb", 32) # name, size
symbolic_bv += 10
symbolic_bv *= 42
symbolic_bv = symbolic_bv.SignExt(32)
print(symbolic_bv) # <BVExpr64 SignExt(32, (symb + 10)*42)>
print(symbolic_bv + concrete_bv) # <BVExpr64 SignExt(32, (symb + 10)*42) + 763392414>The current active state is accessible through the python console using:
import seninja
s = seninja.get_current_state()The state object is an abstraction of the machine and holds the information about memory, registers, files, etc. It also holds the constraints accumulated during the execution.
state.regs holds the register values of the current architecture. Assuming an x86_64 arch:
import seninja
s = seninja.get_current_state()
print(s.regs.rax) # Prints the value of `rax` in the current state. For example `<BVS64 rax_init>`
s.regs.rax = seninja.BVV(0, 64) # Sets the value of `rax` to the value `0`
s.regs.rbx = seninja.BVS("b", 64) # Sets the value of `rbx` to the symbol "b"
s.regs.rbx += s.regs.rax
print(s.regs.rbx * 2) # <BVExpr64 b*2>
print(s.regs.ebx) # <BVExpr32 Extract(31, 0, b)>state.mem holds the memory of the state. Assuming an x86_64 arch:
import seninja
s = seninja.get_current_state()
buf = s.mem.allocate(100) # Allocate 100 bytes in the current state
s.mem.store(buf, seninja.BVV(10, 32), 'little') # Store 10 at address `buf` in little endian
s.mem.store(buf+4, seninja.str_to_bv("ciao")) # Store the string "ciao" at address buf+4
s.mem.store(buf+8, seninja.str_to_bv("ciao", True)) # Store the zero-terminated string "ciao\x00" at address buf+8
print(s.mem.load(buf, 4)) # <BVV32 0x0a000000> (big endian by default)
print(s.mem.load(buf, 4, 'little')) # <BVV32 0x0000000a>
print(s.mem.load(buf, 13)) # <BVV104 0x0a0000006369616f6369616f00>
s.mem.store(s.regs.rdi, seninja.str_to_bv("ciao", True)) # Store the string "ciao\x00" at the address stored in rdistate.os holds information about the operating system, for example files.
import seninja
s = seninja.get_current_state()
fd = s.os.open("/home/luca/a.txt", "rw-") # open the file "/home/luca/a.txt" with permissions "rw-".
# It will be filled with symbols
s.os.write(fd, s.os.write(fd, seninja.str_to_bv_list("ciao"))) # Write the string "ciao" in the file
s.os.seek(fd, 0) # Seek to the first byte
print(s.os.read(fd, 5)) # [<BVV8 0x63>, <BVV8 0x69>, <BVV8 0x61>, <BVV8 0x6f>, <BVS8 unconstrained_/home/luca/a.txt_4>]
s.os.write(s.os.stdin_fd, # write "\x00\x01\x02" to stdin
[seninja.BVV(0, 8), seninja.BVV(1, 8), seninja.BVV(2, 8)])
s.os.seek(s.os.stdin_fd, 0) # seek stdin to zerostate.solver holds the solver of the state. The solver can be used to solve queries using the path constraint of the state.
import seninja
s = seninja.get_current_state()
print(s.solver.assertions) # Print the path constraint of the state. Ex:
# [
# <BoolExpr fsbase_init == 6104>,
# <BoolExpr And(Extract(7, 4, a) == 0, b == 0, c == 0, d == 0, ULE(Extract(3, 0, a), 14))>
# ]
print(s.regs.rdi) # <BVExpr64 Concat(0, d, c, b, a)>
print(s.regs.di) # <BVExpr16 Concat(b, a)>
print(s.solver.evaluate(s.regs.di)) # <BVV16 0x0000>
print(s.solver.evaluate_upto(s.regs.di, 4)) # [<BVV16 0x0007>, <BVV16 0x0005>, <BVV16 0x0001>, <BVV16 0x0009>]
print(s.solver.min(s.regs.di)) # 0
print(s.solver.max(s.regs.di)) # 14
print(s.solver.satisfiable(extra_constraints=[s.regs.di == 15])) # False
print(s.solver.satisfiable(extra_constraints=[s.regs.di == 14])) # Truestate.arch holds the info about the arch of the state. Assuming an x86_64 arch:
print(s.arch.bits()) # 64
print(s.arch.endness()) # little
print(s.arch.get_stack_pointer_reg()) # rsp
print(s.arch.reg_names()) # ['rip', 'rsp', 'rbp', 'rax', 'rbx', 'rcx', 'rdx', 'rsi', 'rdi', ...]