angr_tutorial.py

import angr
import claripy

# Create a new project with the ./angry binary
project = angr.Project('./angry')

# It's OK if this is a (reasonable) overestimate, but
# it cannot be an underestimate.
flag_len = 50

# The following code creates a BVS (symbolic bit vector) which
# represents our sigpwny{...} input to the command line. There are flag_len
# bytes, so there are 8 * flag_len bits in our BVS. We will use angr
# to solve for what these bits should be, given our constraints later.

# First, create an array of symbolic bit vectors of length 8.
# These are all the symbolic characters of our flag.
flag_chars = [claripy.BVS('flag_char_%d' % i, 8) for i in range(flag_len)]

# Then, concatenate all the individual flag characters into one big
# symbolic bit vector.
symbolic_flag = claripy.Concat(*flag_chars)

# Prepare our argv array, the inputs from the command line.
# The first is always the filename of the program, and the
# second is our sigpwny{...} flag.
argv = [project.filename, symbolic_flag]

# This is the start state of the program. It is the entry
# state where its argv are the 2 specified above. You can
# easily adapt this script to provide our flag to stdin instead using
# state = project.factory.full_init_state(stdin=claripy.Concat(symbolic_flag, claripy.BVV(b'\n')))
# and by not allowing null bytes like we do below.
state = project.factory.full_init_state(args=argv)

# Add our constraints to each individual flag character
for flag_char in flag_chars:
    character_is_printable = claripy.And(flag_char >= 0x20, flag_char <= 0x7f)
    character_is_null_byte = flag_char == 0x00

    # We want our flag to be printable. We add that it can also be 0x00,
    # since we overestimated flag_len and 0x00 indicates the string ends.
    # You don't need the null condition if you know flag_len == true flag length
    state.solver.add(claripy.Or(character_is_printable, character_is_null_byte))

# Create a simulation manager given the starting state
simgr = project.factory.simulation_manager(state)

# Look for paths of the program where it prints correct to stdout!
# You can also look for states such that "incorrect" is not printed,
# but then you must add additional constraints for edge cases like
# symbolic_flag is not all 0x00
simgr.explore(find=lambda s: b'That flag is correct! Congrats.' in s.posix.dumps(1))

# For all the found states where incorrect is not printed given our input,
for found in simgr.found:
    # Solve for the bits of our symbolic_flag and print them as bytes!
    print(found.solver.eval(symbolic_flag, cast_to=bytes))