# Angr - Examples {% hint style="info" %} If the program is using **`scanf`** to get **several values at once from stdin** you need to generate a state that starts after the **`scanf`**. {% endhint %} ### Input to reach address \(indicating the address\) ```python 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) ``` ### Input to reach address \(indicating prints\) ```python # 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) ``` ### Registry values ```python # 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) ``` ### Stack values ```python # 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) ``` In this scenario, the input was taken with `scanf("%u %u")` and the value `"1 1"` was given, so the values **`0x00000001`** of the stack come from the **user input**. You can see how this values starts in `$ebp - 8`. Therefore, in the code we have **subtracted 8 bytes to `$esp` \(as in that moment `$ebp` and `$esp` had the same value\)** and then we have pushed the BVS. ![](../../../.gitbook/assets/image%20%28613%29.png) ### Static Memory values \(Global variables\) ```python 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) ``` ### Dynamic Memory Values \(Malloc\) ```python 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) ``` ### File Simulation ```python #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) ``` {% hint style="info" %} Note that the symbolic file could also contain constant data merged with symbolic data: ```python # 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. # (!) ``` {% endhint %} ### Applying Constrains {% hint style="info" %} Sometimes simple human operations like compare 2 words of length 16 **char by char** \(loop\), **cost** a lot to a **angr** because it needs to generate branches **exponentially** because it generates 1 branch per if: `2^16` Therefore, it's easier to **ask angr get to a previous point** \(where the real difficult part was already done\) and **set those constrains manually**. {% endhint %} ```python # 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