nathanfarlow · October 10, 2021 18:58
diff --git a/angr_tutorial.py b/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))
	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))