using library angr

Author: MinKuanIsHere

lab8/solve.py

@@ -1,51 +1,61 @@
 #!/usr/bin/env python3
 
+import angr
+import claripy
+import logging
+logging.getLogger('angr').setLevel(logging.ERROR)
 import sys
-
-# Fallback for environments without angr (e.g., CI)
-try:
-    import angr
-    import claripy
-    HAS_ANGR = True
-except ModuleNotFoundError:
-    HAS_ANGR = False
+import os
 
 def main():
-    if not HAS_ANGR:
-        # Fallback: Output known good 8-byte binary key
-        fallback_key = bytes([0x15, 0x40, 0x5d, 0x6b, 0xf2, 0xd6, 0xfc, 0xfb])
-        sys.stdout.buffer.write(fallback_key)
-        sys.exit(0)
-
-    # Load target binary without external library loading
+    # Check if ./chal exists
+    if not os.path.isfile('./chal'):
+        print("Error: './chal' binary not found. Run 'make' to compile it.", file=sys.stderr)
+        sys.exit(1)
+    
+    # Load the binary
     try:
-        proj = angr.Project("./chal", auto_load_libs=False)
+        proj = angr.Project('./chal', auto_load_libs=False)
     except Exception as e:
-        print(f"Error loading binary: {e}. Run 'make' to compile it.", file=sys.stderr)
+        print(f"Error loading binary: {e}", file=sys.stderr)
         sys.exit(1)
-
-    # Declare symbolic variables (8 bytes)
-    sym_len = 8
-    sym_chars = [claripy.BVS(f'sym_{i}', 8) for i in range(sym_len)]
-    sym_input = claripy.Concat(*sym_chars)  # 8 bytes, no \0
-
-    # Prepare initial program state with symbolic input
-    init_state = proj.factory.entry_state(
-        stdin=sym_input,
-        add_options={angr.options.ZERO_FILL_UNCONSTRAINED_MEMORY}
-    )
-
-    # Start symbolic exploration
-    sim_mgr = proj.factory.simgr(init_state)
-    sim_mgr.explore(
-        find=lambda s: b"flag is:" in s.posix.dumps(1),
-        avoid=lambda s: b"Wrong key!" in s.posix.dumps(1)
-    )
-
-    # Extract and print result if a successful state is found
-    if sim_mgr.found:
-        result = sim_mgr.found[0].solver.eval(sym_input, cast_to=bytes)
-        sys.stdout.buffer.write(result[:sym_len])
+    
+    # Create symbolic input (8 bytes)
+    input_chars = [claripy.BVS(f'char_{i}', 8) for i in range(8)]
+    
+    # Create initial state with symbolic input on stdin
+    state = proj.factory.entry_state(stdin=claripy.Concat(*input_chars))
+    
+    # Constrain input to printable ASCII (32-126)
+    for c in input_chars:
+        state.solver.add(c >= 32)
+        state.solver.add(c <= 126)
+    
+    # Create simulation manager
+    simgr = proj.factory.simulation_manager(state)
+    
+    # Explore to find the path that prints the flag
+    def is_successful(state):
+        stdout_content = state.posix.dumps(1)  # Check stdout
+        return b"Correct!" in stdout_content
+    
+    def is_failed(state):
+        stdout_content = state.posix.dumps(1)
+        return b"Wrong key!" in stdout_content
+    
+    simgr.explore(find=is_successful, avoid=is_failed)
+    
+    # Check if a successful state was found
+    if simgr.found:
+        found_state = simgr.found[0]
+        # Extract concrete values for the input
+        secret_key = b""
+        for c in input_chars:
+            val = found_state.solver.eval(c)
+            secret_key += bytes([val])
+        
+        # Output the secret key to stdout
+        sys.stdout.buffer.write(secret_key)
     else:
         print("No solution found!", file=sys.stderr)
         sys.exit(1)