Angr - Examples

Support HackTricks

рдпрджрд┐ рдкреНрд░реЛрдЧреНрд░рд╛рдо scanf рдХрд╛ рдЙрдкрдпреЛрдЧ рдХрд░рдХреЗ stdin рд╕реЗ рдПрдХ рд╕рд╛рде рдХрдИ рдорд╛рди рдкреНрд░рд╛рдкреНрдд рдХрд░ рд░рд╣рд╛ рд╣реИ рддреЛ рдЖрдкрдХреЛ рдПрдХ рдРрд╕рд╛ рд░рд╛рдЬреНрдп рдЙрддреНрдкрдиреНрди рдХрд░рдиреЗ рдХреА рдЖрд╡рд╢реНрдпрдХрддрд╛ рд╣реИ рдЬреЛ scanf рдХреЗ рдмрд╛рдж рд╢реБрд░реВ рд╣реЛрддрд╛ рд╣реИред

Codes taken from https://github.com/jakespringer/angr_ctf

Input to reach address (indicating the address)

import angr
import sys

def main(argv):
path_to_binary = argv[1]  # :string
project = angr.Project(path_to_binary)

# Start in main()
initial_state = project.factory.entry_state()
# Start simulation
simulation = project.factory.simgr(initial_state)

# Find the way yo reach the good address
good_address = 0x804867d

# Avoiding this address
avoid_address = 0x080485A8
simulation.explore(find=good_address, avoid=avoid_address)

# If found a way to reach the address
if simulation.found:
solution_state = simulation.found[0]

# Print the string that Angr wrote to stdin to follow solution_state
print(solution_state.posix.dumps(sys.stdin.fileno()))
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рдкрддреЗ рддрдХ рдкрд╣реБрдБрдЪрдиреЗ рдХреЗ рд▓рд┐рдП рдЗрдирдкреБрдЯ (рдкреНрд░рд┐рдВрдЯреНрд╕ рдХреЛ рдЗрдВрдЧрд┐рдд рдХрд░рдирд╛)

# If you don't know the address you want to recah, but you know it's printing something
# You can also indicate that info

import angr
import sys

def main(argv):
path_to_binary = argv[1]
project = angr.Project(path_to_binary)
initial_state = project.factory.entry_state()
simulation = project.factory.simgr(initial_state)

def is_successful(state):
#Successful print
stdout_output = state.posix.dumps(sys.stdout.fileno())
return b'Good Job.' in stdout_output

def should_abort(state):
#Avoid this print
stdout_output = state.posix.dumps(sys.stdout.fileno())
return b'Try again.' in stdout_output

simulation.explore(find=is_successful, avoid=should_abort)

if simulation.found:
solution_state = simulation.found[0]
print(solution_state.posix.dumps(sys.stdin.fileno()))
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рд░рдЬрд┐рд╕реНрдЯреНрд░реА рдорд╛рди

# Angr doesn't currently support reading multiple things with scanf (Ex:
# scanf("%u %u).) You will have to tell the simulation engine to begin the
# program after scanf is called and manually inject the symbols into registers.

import angr
import claripy
import sys

def main(argv):
path_to_binary = argv[1]
project = angr.Project(path_to_binary)

# Address were you want to indicate the relation BitVector - registries
start_address = 0x80488d1
initial_state = project.factory.blank_state(addr=start_address)


# Create Bit Vectors
password0_size_in_bits = 32  # :integer
password0 = claripy.BVS('password0', password0_size_in_bits)

password1_size_in_bits = 32  # :integer
password1 = claripy.BVS('password1', password1_size_in_bits)

password2_size_in_bits = 32  # :integer
password2 = claripy.BVS('password2', password2_size_in_bits)

# Relate it Vectors with the registriy values you are interested in to reach an address
initial_state.regs.eax = password0
initial_state.regs.ebx = password1
initial_state.regs.edx = password2

simulation = project.factory.simgr(initial_state)

def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output

def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output

simulation.explore(find=is_successful, avoid=should_abort)

if simulation.found:
solution_state = simulation.found[0]

solution0 = solution_state.solver.eval(password0)
solution1 = solution_state.solver.eval(password1)
solution2 = solution_state.solver.eval(password2)

# Aggregate and format the solutions you computed above, and then print
# the full string. Pay attention to the order of the integers, and the
# expected base (decimal, octal, hexadecimal, etc).
solution = ' '.join(map('{:x}'.format, [ solution0, solution1, solution2 ]))  # :string
print(solution)
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рд╕реНрдЯреИрдХ рдорд╛рди

# Put bit vectors in th stack to find out the vallue that stack position need to
# have to reach a rogram flow

import angr
import claripy
import sys

def main(argv):
path_to_binary = argv[1]
project = angr.Project(path_to_binary)

# Go to some address after the scanf where values have already being set in the stack
start_address = 0x8048697
initial_state = project.factory.blank_state(addr=start_address)

# Since we are starting after scanf, we are skipping this stack construction
# step. To make up for this, we need to construct the stack ourselves. Let us
# start by initializing ebp in the exact same way the program does.
initial_state.regs.ebp = initial_state.regs.esp

# In this case scanf("%u %u") is used, so 2 BVS are going to be needed
password0 = claripy.BVS('password0', 32)
password1 = claripy.BVS('password1', 32)

# Now, in the address were you have stopped, check were are the scanf values saved
# Then, substrack form the esp registry the needing padding to get to the
# part of the stack were the scanf values are being saved and push the BVS
# (see the image below to understan this -8)
padding_length_in_bytes = 8  # :integer
initial_state.regs.esp -= padding_length_in_bytes

initial_state.stack_push(password0)
initial_state.stack_push(password1)

simulation = project.factory.simgr(initial_state)

def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output

def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output

simulation.explore(find=is_successful, avoid=should_abort)

if simulation.found:
solution_state = simulation.found[0]

solution0 = solution_state.solver.eval(password0)
solution1 = solution_state.solver.eval(password1)

solution = ' '.join(map(str, [ solution0, solution1 ]))
print(solution)
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рдЗрд╕ рдкрд░рд┐рджреГрд╢реНрдп рдореЗрдВ, рдЗрдирдкреБрдЯ scanf("%u %u") рдХреЗ рд╕рд╛рде рд▓рд┐рдпрд╛ рдЧрдпрд╛ рдерд╛ рдФрд░ рдорд╛рди "1 1" рджрд┐рдпрд╛ рдЧрдпрд╛ рдерд╛, рдЗрд╕рд▓рд┐рдП рд╕реНрдЯреИрдХ рдХреЗ рдорд╛рди 0x00000001 рдЙрдкрдпреЛрдЧрдХрд░реНрддрд╛ рдЗрдирдкреБрдЯ рд╕реЗ рдЖрддреЗ рд╣реИрдВред рдЖрдк рджреЗрдЦ рд╕рдХрддреЗ рд╣реИрдВ рдХрд┐ рдпреЗ рдорд╛рди $ebp - 8 рд╕реЗ рд╢реБрд░реВ рд╣реЛрддреЗ рд╣реИрдВред рдЗрд╕рд▓рд┐рдП, рдХреЛрдб рдореЗрдВ рд╣рдордиреЗ $esp рд╕реЗ 8 рдмрд╛рдЗрдЯ рдШрдЯрд╛рдП (рдЬреИрд╕реЗ рдЙрд╕ рд╕рдордп $ebp рдФрд░ $esp рдХрд╛ рд╡рд╣реА рдорд╛рди рдерд╛) рдФрд░ рдлрд┐рд░ рд╣рдордиреЗ BVS рдХреЛ рдкреБрд╢ рдХрд┐рдпрд╛ред

рд╕реНрдерд┐рд░ рдореЗрдореЛрд░реА рдорд╛рди (рд╡реИрд╢реНрд╡рд┐рдХ рдЪрд░)

import angr
import claripy
import sys

def main(argv):
path_to_binary = argv[1]
project = angr.Project(path_to_binary)

#Get an address after the scanf. Once the input has already being saved in the memory positions
start_address = 0x8048606
initial_state = project.factory.blank_state(addr=start_address)

# The binary is calling scanf("%8s %8s %8s %8s").
# So we need 4 BVS of size 8*8
password0 = claripy.BVS('password0', 8*8)
password1 = claripy.BVS('password1', 8*8)
password2 = claripy.BVS('password2', 8*8)
password3 = claripy.BVS('password3', 8*8)

# Write the symbolic BVS in the memory positions
password0_address = 0xa29faa0
initial_state.memory.store(password0_address, password0)
password1_address = 0xa29faa8
initial_state.memory.store(password1_address, password1)
password2_address = 0xa29fab0
initial_state.memory.store(password2_address, password2)
password3_address = 0xa29fab8
initial_state.memory.store(password3_address, password3)

simulation = project.factory.simgr(initial_state)

def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output

def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output

simulation.explore(find=is_successful, avoid=should_abort)

if simulation.found:
solution_state = simulation.found[0]

# Get the values the memory addresses should store
solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode()
solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode()
solution2 = solution_state.solver.eval(password2,cast_to=bytes).decode()
solution3 = solution_state.solver.eval(password3,cast_to=bytes).decode()

solution = ' '.join([ solution0, solution1, solution2, solution3 ])

print(solution)
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рдбрд╛рдпрдирд╛рдорд┐рдХ рдореЗрдореЛрд░реА рдорд╛рди (Malloc)

import angr
import claripy
import sys

def main(argv):
path_to_binary = argv[1]
project = angr.Project(path_to_binary)

# Get address after scanf
start_address = 0x804869e
initial_state = project.factory.blank_state(addr=start_address)

# The binary is calling scanf("%8s %8s") so 2 BVS are needed.
password0 = claripy.BVS('password0', 8*8)
password1 = claripy.BVS('password0', 8*8)

# Find a coupble of addresses that aren't used by the binary (like 0x4444444 & 0x4444454)
# The address generated by mallosc is going to be saved in some address
# Then, make that address point to the fake heap addresses were the BVS are going to be saved
fake_heap_address0 = 0x4444444
pointer_to_malloc_memory_address0 = 0xa79a118
initial_state.memory.store(pointer_to_malloc_memory_address0, fake_heap_address0, endness=project.arch.memory_endness)
fake_heap_address1 = 0x4444454
pointer_to_malloc_memory_address1 = 0xa79a120
initial_state.memory.store(pointer_to_malloc_memory_address1, fake_heap_address1, endness=project.arch.memory_endness)

# Save the VBS in the new fake heap addresses created
initial_state.memory.store(fake_heap_address0, password0)
initial_state.memory.store(fake_heap_address1, password1)

simulation = project.factory.simgr(initial_state)

def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output

def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output

simulation.explore(find=is_successful, avoid=should_abort)

if simulation.found:
solution_state = simulation.found[0]

solution0 = solution_state.solver.eval(password0,cast_to=bytes).decode()
solution1 = solution_state.solver.eval(password1,cast_to=bytes).decode()

solution = ' '.join([ solution0, solution1 ])

print(solution)
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рдлрд╝рд╛рдЗрд▓ рд╕рд┐рдореБрд▓реЗрд╢рди

#In this challenge a password is read from a file and we want to simulate its content

import angr
import claripy
import sys

def main(argv):
path_to_binary = argv[1]
project = angr.Project(path_to_binary)

# Get an address just before opening the file with th simbolic content
# Or at least when the file is not going to suffer more changes before being read
start_address = 0x80488db
initial_state = project.factory.blank_state(addr=start_address)

# Specify the filena that is going to open
# Note that in theory, the filename could be symbolic.
filename = 'WCEXPXBW.txt'
symbolic_file_size_bytes = 64

# Create a BV which is going to be the content of the simbolic file
password = claripy.BVS('password', symbolic_file_size_bytes * 8)

# Create the file simulation with the simbolic content
password_file = angr.storage.SimFile(filename, content=password)

# Add the symbolic file we created to the symbolic filesystem.
initial_state.fs.insert(filename, password_file)

simulation = project.factory.simgr(initial_state)

def is_successful(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Good Job.'.encode() in stdout_output

def should_abort(state):
stdout_output = state.posix.dumps(sys.stdout.fileno())
return 'Try again.'.encode() in stdout_output

simulation.explore(find=is_successful, avoid=should_abort)

if simulation.found:
solution_state = simulation.found[0]

solution = solution_state.solver.eval(password,cast_to=bytes).decode()

print(solution)
else:
raise Exception('Could not find the solution')

if __name__ == '__main__':
main(sys.argv)

рдзреНрдпрд╛рди рджреЗрдВ рдХрд┐ рдкреНрд░рддреАрдХрд╛рддреНрдордХ рдлрд╝рд╛рдЗрд▓ рдореЗрдВ рдкреНрд░рддреАрдХрд╛рддреНрдордХ рдбреЗрдЯрд╛ рдХреЗ рд╕рд╛рде рдорд┐рд╢реНрд░рд┐рдд рд╕реНрдерд┐рд░рд╛рдВрдХ рдбреЗрдЯрд╛ рднреА рд╣реЛ рд╕рдХрддрд╛ рд╣реИ:

# Hello world, my name is John.
# ^                       ^
# ^ address 0             ^ address 24 (count the number of characters)
# In order to represent this in memory, we would want to write the string to
# the beginning of the file:
#
# hello_txt_contents = claripy.BVV('Hello world, my name is John.', 30*8)
#
# Perhaps, then, we would want to replace John with a
# symbolic variable. We would call:
#
# name_bitvector = claripy.BVS('symbolic_name', 4*8)
#
# Then, after the program calls fopen('hello.txt', 'r') and then
# fread(buffer, sizeof(char), 30, hello_txt_file), the buffer would contain
# the string from the file, except four symbolic bytes where the name would be
# stored.
# (!)

Applying Constrains

рдХрднреА-рдХрднреА рд╕рд░рд▓ рдорд╛рдирд╡ рд╕рдВрдЪрд╛рд▓рди рдЬреИрд╕реЗ 16 рд▓рдВрдмрд╛рдИ рдХреЗ 2 рд╢рдмреНрджреЛрдВ рдХреА рддреБрд▓рдирд╛ рдХрд░рдирд╛ char by char (рд▓реВрдк), angr рдХреЗ рд▓рд┐рдП рдмрд╣реБрдд рдорд╣рдВрдЧрд╛ рд╣реЛрддрд╛ рд╣реИ рдХреНрдпреЛрдВрдХрд┐ рдЗрд╕реЗ рд╢рд╛рдЦрд╛рдПрдБ exponentially рдЙрддреНрдкрдиреНрди рдХрд░рдиреА рд╣реЛрддреА рд╣реИрдВ рдХреНрдпреЛрдВрдХрд┐ рдпрд╣ рдкреНрд░рддреНрдпреЗрдХ if рдкрд░ 1 рд╢рд╛рдЦрд╛ рдЙрддреНрдкрдиреНрди рдХрд░рддрд╛ рд╣реИ: 2^16 рдЗрд╕рд▓рд┐рдП, angr рд╕реЗ рдкрд┐рдЫрд▓реЗ рдмрд┐рдВрджреБ рдкрд░ рдЬрд╛рдиреЗ рдХреЗ рд▓рд┐рдП рдХрд╣рдирд╛ (рдЬрд╣рд╛рдБ рдЕрд╕рд▓реА рдХрдард┐рди рд╣рд┐рд╕реНрд╕рд╛ рдкрд╣рд▓реЗ рд╣реА рдХрд┐рдпрд╛ рдЬрд╛ рдЪреБрдХрд╛ рдерд╛) рдФрд░ рдЙрди constrains рдХреЛ рдореИрдиреНрдпреБрдЕрд▓ рд░реВрдк рд╕реЗ рд╕реЗрдЯ рдХрд░рдирд╛ рдЖрд╕рд╛рди рд╣реЛрддрд╛ рд╣реИред

# After perform some complex poperations to the input the program checks
# char by char the password against another password saved, like in the snippet:
#
# #define REFERENCE_PASSWORD = "AABBCCDDEEFFGGHH";
# int check_equals_AABBCCDDEEFFGGHH(char* to_check, size_t length) {
#   uint32_t num_correct = 0;
#   for (int i=0; i<length; ++i) {
#     if (to_check[i] == REFERENCE_PASSWORD[i]) {
#       num_correct += 1;
#     }
#   }
#   return num_correct == length;
# }
#
# ...
#
# char* input = user_input();
# char* encrypted_input = complex_function(input);
# if (check_equals_AABBCCDDEEFFGGHH(encrypted_input, 16)) {
#   puts("Good Job.");