> For the complete documentation index, see [llms.txt](https://the-winrars.gitbook.io/references/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://the-winrars.gitbook.io/references/reverse-engineering/tools/angr.md).

# Angr

[Angr](https://github.com/angr/angr) is a powerful binary analysis framework which has come in handy several times in CTFs. It does a huge amount of stuff, so I'm only going to cover the few things I've used it for.

### Symbolic Execution

Angr can analyse binaries by inputting 'symbols' rather than literal text. What happens to these symbols (comparisons, transformations) is then recorded, allowing us to get a picture of what a binary is doing. The main usage I've gotten out of this is flag-checker challenges, where we are expected to enter a flag, our input goes through a series of transformations, and is compared against a constant to check if the entered value is correct. Here's a script I used to solve Beginner from Google CTF 2020.

```python
import angr, claripy
target = angr.Project('a.out', auto_load_libs=False)
input_len = 15 # Discovered with manual analysis at a glance
inp = [claripy.BVS('flag_%d' %i, 8) for i in range(input_len)]
# Define an array of 8 bit vectors ffor each char of the flag
flag = claripy.Concat(*inp + [claripy.BVV(b'\n')])

st = target.factory.full_init_state(args=["./a.out"], stdin=flag)
# Create a simulation with our flag symbols as stdin
for k in inp:
    st.solver.add(k < 0x7f)
    st.solver.add(k > 0x20)
# Add constraints that the characters should be printable

sm = target.factory.simulation_manager(st)
sm.run()
y = []
for x in sm.deadended:
    # Out of the simulations that exit, record
    # any that output SUCCESS
    if b"SUCCESS" in x.posix.dumps(1):
        y.append(x)

#grab the first ouptut
valid = y[0].posix.dumps(0)
print(valid)
```

This particular example isn't great, as it is basically a brute force, as I was just getting to learn angr. However, it shows how easy it makes it for challenges with light brute forcing.

Here's a better example: Beginner Rev from Fword CTF

```python
import angr
import claripy #the solver engine

proj = angr.Project("./welcome", auto_load_libs=False)
sym_arg_size = 0x10 #Length in Bytes because we will multiply with 8 later
inp = [claripy.BVS('flag_%d' % i, 8 ) for i in range(sym_arg_size)]
flag = claripy.Concat(*inp + [claripy.BVV(b'\n')])
state = proj.factory.full_init_state(args=["./welcome"], stdin=flag)
for byte in inp:
    state.solver.add(byte >= ord('0'))
    state.solver.add(byte <= ord('9'))
# Input is specified to be a number
simgr = proj.factory.simulation_manager(state)
good = 0x400000 + 0x12b2
# Address of flag file being opened
bad = [0x400000 + 0x1669, 0x400000 + 0x167b]
# Addresses of failure messages being printed
simgr.use_technique(angr.exploration_techniques.DFS())
simgr.explore(find=good, avoid=bad)
# Explore input that will end at the good while avoiding the bad
found = simgr.found[0]
print(found.solver.eval(flag, cast_to=bytes))
# Cast our found input to bytes and print
```

This is a much more intelligent way of exploring the binary, and printed `1755121917194838` after only 20 seconds.