A radare2 Plugin to perform symbolic execution with a simple macro call. Internally it uses angr as execution engine. The Usage is possible with and without debugger, dynamic and static analysis mode.
To "install" it just create r2-macros in your .radare2rc file with the according path to the r4ge files.
Requirements are of course angr and radare2 and also termcolor which is used for colored printing.
main plugin file, performs static and dynamic analysis
(r4ge, #!pipe python2.7 /pathToFile/r4ge.py)mark a specific memory region as symbolic (addr: start address, bytes: how many bytes, name: name the variable)
(markMemSymbolic addr bytes name, #!pipe python2.7 /pathToFile/createVariable.py symb $0 $1 $2)create hooks in r2 and patch function calls or other statements (syntax of the instructions: rax=0x4 or rax=0x4;rbx=0x10)
(addHook addr instructions bytes comment, #!pipe python2.7 /pathToFile/createVariable.py hook $0 $1
$2 $3)create asserts to check register values during exploration (syntax of the instructions: rax==0x3 or rax#=0x3;rax<=0x10) Note: # is used instead of >, cause r2 uses > as pipe operator.
(addAssert addr assertions bytes comment, #!pipe python2.7 /pathToFile/createVariable.py assert $0
$1 $2)create an angr script out of the current r2 session
(createScript name, #!pipe python2.7 /pathToFile/createScript.py $0)call a function and set the return value (currently in development mode)
(callFunction retval, #!pipe python2.7 /pathToFile/callFunction.py $0)The dynamic mode will print the conrectized symbolic memory if it found a path, the static mode will open an IPython shell in r2 and you will have to concrete the memory by yourself.
In r2 just create the flags with the name: r4ge.start (only needed in static mode), r4ge.find, r4ge.avoidx (where x is a increasing number, it is not possible in r2 to create flags with the same name) After the flag creation, create Hooks or Asserts if you need one and afterwards just call the r4ge macro.
do not hesitate to ask or write us an email ;)