From f84973969b9f5848e085591c160344770256fdf5 Mon Sep 17 00:00:00 2001 From: Zryxion <90599845+Zryxion@users.noreply.github.com> Date: Sun, 18 May 2025 14:00:01 +0800 Subject: [PATCH 1/4] Update solve.py --- lab8/solve.py | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/lab8/solve.py b/lab8/solve.py index 9ab3ee2..1b5f226 100755 --- a/lab8/solve.py +++ b/lab8/solve.py @@ -1,11 +1,45 @@ #!/usr/bin/env python3 -import angr,sys +import angr +import sys def main(): - secret_key = b"" - sys.stdout.buffer.write(secret_key) + project = angr.Project('./chal', auto_load_libs=False) + # Allocate 8 symbolic bytes for the input + input_len = 8 + input_addr = 0x404000 # Arbitrary writable memory address + state = project.factory.entry_state() + + # Create symbolic variables and store them in memory + for i in range(input_len): + sym_byte = state.solver.BVS(f'input_{i}', 8) + state.memory.store(input_addr + i, sym_byte) + # Constrain input to printable characters (excluding newline) + state.solver.add(sym_byte >= 0x20) + state.solver.add(sym_byte <= 0x7e) + + # Store null terminator to simulate stripped newline in fgets + state.memory.store(input_addr + input_len, state.solver.BVV(0, 8)) + + # Overwrite return address of fgets so input goes where main expects + state.globals['input_addr'] = input_addr + state.regs.rdi = input_addr # input pointer to gate(input) + + # Call gate function directly + gate_func = project.loader.find_symbol('gate').rebased_addr + simgr = project.factory.simgr(state) + simgr.explore(find=gate_func + 100) # explore a bit past gate() + + for found in simgr.found: + result = b'' + for i in range(input_len): + c = found.solver.eval(found.memory.load(input_addr + i, 1), cast_to=bytes) + result += c + sys.stdout.buffer.write(result + b'\n') + return + + print("No solution found.") if __name__ == '__main__': main() From c97ea3feb480c98eb99c158cbb9ab31ad0cd3ea2 Mon Sep 17 00:00:00 2001 From: Zryxion <90599845+Zryxion@users.noreply.github.com> Date: Mon, 19 May 2025 16:09:45 +0800 Subject: [PATCH 2/4] Update solve.py --- lab8/solve.py | 67 ++++++++++++++++++++++++++------------------------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/lab8/solve.py b/lab8/solve.py index 1b5f226..1909ccb 100755 --- a/lab8/solve.py +++ b/lab8/solve.py @@ -1,45 +1,46 @@ #!/usr/bin/env python3 import angr +import claripy import sys def main(): + # Create an angr project project = angr.Project('./chal', auto_load_libs=False) - # Allocate 8 symbolic bytes for the input + # Declare a symbolic input of 8 bytes (the correct input length) input_len = 8 - input_addr = 0x404000 # Arbitrary writable memory address - state = project.factory.entry_state() - - # Create symbolic variables and store them in memory - for i in range(input_len): - sym_byte = state.solver.BVS(f'input_{i}', 8) - state.memory.store(input_addr + i, sym_byte) - # Constrain input to printable characters (excluding newline) - state.solver.add(sym_byte >= 0x20) - state.solver.add(sym_byte <= 0x7e) - - # Store null terminator to simulate stripped newline in fgets - state.memory.store(input_addr + input_len, state.solver.BVV(0, 8)) - - # Overwrite return address of fgets so input goes where main expects - state.globals['input_addr'] = input_addr - state.regs.rdi = input_addr # input pointer to gate(input) - - # Call gate function directly - gate_func = project.loader.find_symbol('gate').rebased_addr - simgr = project.factory.simgr(state) - simgr.explore(find=gate_func + 100) # explore a bit past gate() - - for found in simgr.found: - result = b'' - for i in range(input_len): - c = found.solver.eval(found.memory.load(input_addr + i, 1), cast_to=bytes) - result += c - sys.stdout.buffer.write(result + b'\n') - return - - print("No solution found.") + input_chars = [claripy.BVS(f'input_{i}', 8) for i in range(input_len)] + input_expr = claripy.Concat(*input_chars) + + # Set up the initial state with symbolic stdin + state = project.factory.full_init_state( + args=['./chal'], + stdin=input_expr + ) + + # Constrain each input character to be printable and not newline + for char in input_chars: + state.solver.add(char >= 0x20) + state.solver.add(char <= 0x7e) + + # Create a simulation manager + simgr = project.factory.simulation_manager(state) + + # Define what we're looking for: the success message + def is_successful(state): + return b'Correct! The flag is:' in state.posix.dumps(1) + + # Explore paths + simgr.explore(find=is_successful) + + if simgr.found: + found = simgr.found[0] + # Extract the concrete value of the symbolic input + solution = found.solver.eval(input_expr, cast_to=bytes) + sys.stdout.buffer.write(solution + b'\n') + else: + print("No solution found.") if __name__ == '__main__': main() From 6136e69a252626f5043ffcb6c1f49a3223c51feb Mon Sep 17 00:00:00 2001 From: Zryxion <90599845+Zryxion@users.noreply.github.com> Date: Mon, 19 May 2025 16:14:50 +0800 Subject: [PATCH 3/4] Update solve.py --- lab8/solve.py | 6 ------ 1 file changed, 6 deletions(-) diff --git a/lab8/solve.py b/lab8/solve.py index 1909ccb..4d7e90e 100755 --- a/lab8/solve.py +++ b/lab8/solve.py @@ -5,29 +5,23 @@ import sys def main(): - # Create an angr project project = angr.Project('./chal', auto_load_libs=False) - # Declare a symbolic input of 8 bytes (the correct input length) input_len = 8 input_chars = [claripy.BVS(f'input_{i}', 8) for i in range(input_len)] input_expr = claripy.Concat(*input_chars) - # Set up the initial state with symbolic stdin state = project.factory.full_init_state( args=['./chal'], stdin=input_expr ) - # Constrain each input character to be printable and not newline for char in input_chars: state.solver.add(char >= 0x20) state.solver.add(char <= 0x7e) - # Create a simulation manager simgr = project.factory.simulation_manager(state) - # Define what we're looking for: the success message def is_successful(state): return b'Correct! The flag is:' in state.posix.dumps(1) From 691b9a63e77492c5e6a9b72fcff85a5e9e0b585d Mon Sep 17 00:00:00 2001 From: Zryxion <90599845+Zryxion@users.noreply.github.com> Date: Mon, 19 May 2025 22:47:46 +0800 Subject: [PATCH 4/4] Update solve.py --- lab8/solve.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lab8/solve.py b/lab8/solve.py index 4d7e90e..24fb102 100755 --- a/lab8/solve.py +++ b/lab8/solve.py @@ -4,7 +4,7 @@ import claripy import sys -def main(): +def main(): project = angr.Project('./chal', auto_load_libs=False) input_len = 8