Angr

Bruteforce but smart

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.

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

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.