Binary analysis suite that includes tools for:
- Symbolic Execution
- CFG generation
- ROP gadget finder
angr
angr is a python library that automates this process of finding input constraints. The default searching algorithm it uses is the Breath First Search Algorithm
Installation
the blackarch version does not work.
It is best to make a Python Virtual Environment where you pip install angr automatically
Example Venv
python -m venv angrproj
cd angrproj && source /bin/activate
pip install angr monkeyhex setuptools wheel pip ipython
angr Process
- CLE loads the binary
- archinfo provides information to SimEngine and SimOS about the architecture the binary is running on
- pyvex turns assembly instructions into VEX IR
- SimEngine created to emulate the execution of VEX IR instructions
- SimOS created to emulate the execution environment - whether its Windows or Linux
- claripy turns VEX IR into Bitvectors
- z3 uses the Bitvectors to solve for constraints with its SMT Solver
Angr Script Anatomy
- Loading binary
- Translating binary into IR
- Performing the analysis:
- Partial or full program analysis
- Symbolic Execution
Boilerplate Script
import angr
import claripy
proj = angr.Project("./binaryName") # load binary into an angr project
state = proj.factory.entry_state() # create a generic SimState
simgr = proj.factory.simulation_manager(state) # set the intial state of the simulation to state
simgr.explore(find = lambda newState: b"String in correct output" in newState.posix.dumps(1)) # search for the constraints that result in a string in the correct output
simgr.found[0] # will give us the state
print(simgr.found[0].posix.dumps(0)) # stdin that gives us the correct stdout