Autorev 1 picoCTF 2026 Solution

Description

1. Step 1Receive and analyse the binary
   The challenge sends a binary that checks a password. Use automated tools to quickly identify the correct input.
   bash

   strings ./binary

   Copied!

   bash

   ltrace ./binary somepassword

   Copied!

   bash

   strace ./binary somepassword

   Copied!
   Learn more

   strings extracts all printable character sequences of length ≥4 from a binary. For simple CTF binaries that hardcode the password in plaintext, this single command is often sufficient. ltrace intercepts calls to shared library functions (such as strcmp), printing both arguments - so if the binary calls strcmp(your_input, "secret123"), ltrace reveals secret123 immediately. strace similarly traces system calls.

   These tools work on dynamic binaries that call standard library functions. Stripped or statically linked binaries require a disassembler like Ghidra or Binary Ninja, or a debugger like GDB with break *address to pause at the comparison and inspect registers.

   The challenge is framed as a speed test, which hints at automation. Even basic static analysis (strings + ltrace) can be scripted in a few lines of Python using the subprocess module, making it fast enough for challenges that send a fresh binary each connection.

2. Step 2Use angr for automated reverse engineering
   Symbolic-execute the binary to find the success path. Caveat: angr struggles when input length is unknown or branches are 256-way per byte; pin find/avoid markers and the input length first by reading the binary in Ghidra.
   bash

   pip install angr

   Copied!

   bash

   strings ./binary | grep -iE 'correct|wrong|nice|try|flag'

   Copied!

   python

   python3 << 'EOF'
   import angr, claripy
   
   # auto_load_libs=False skips loading libc into the analysis - dramatically faster
   # and avoids most external-call modeling issues.
   proj = angr.Project("./binary", auto_load_libs=False)
   
   # Pin the input length first. Read the binary statically (Ghidra/strings) to
   # find calls like fgets(buf, 32, stdin) or scanf("%32s", ...). Use that exact
   # byte count - guessing wrong is the #1 reason angr returns no states.
   INPUT_LEN = 32
   password = claripy.BVS("password", 8*INPUT_LEN)
   state = proj.factory.entry_state(stdin=angr.SimFile(content=password+b"\n"))
   
   # Identify success/failure markers from the binary, do not guess:
   #   strings ./binary | grep -iE 'correct|wrong|nice|try|flag'
   # Replace b"picoCTF" / b"Wrong" with the literal markers you find.
   sm = proj.factory.simulation_manager(state)
   sm.explore(find=lambda s: b"picoCTF" in s.posix.dumps(1),
              avoid=lambda s: b"Wrong" in s.posix.dumps(1))
   
   if sm.found:
       sol = sm.found[0]
       print("Password:", sol.solver.eval(password, cast_to=bytes))
       print("Flag:", sol.posix.dumps(1))
   EOF

   Copied!
   Learn more

   angr is a Python binary analysis framework that combines symbolic execution with constraint solving. Instead of running the binary with a concrete input, angr represents the input as a symbolic variable and tracks how each instruction transforms it. When the program reaches a branch, angr forks the execution state, exploring both paths simultaneously.

   auto_load_libs=False tells angr not to load libc and the dynamic linker into its analysis. The default behavior loads everything in ldd output and tries to symbolically execute through it, which is slow (tens of seconds to minutes per project) and frequently introduces unconstrained-state explosions because libc internals often involve syscalls angr can't model precisely. For most CTF binaries, the real logic is in main and angr's built-in SimProcedures for common libc functions (strcmp, scanf, printf) are good enough.

   To find the input length, run strings -a ./binary for format-string hints (e.g., %32s), open the binary in Ghidra and look for the fgets/read/scanf call in main, or just match the printed prompt ("Enter the 32-character password"). The find/avoid markers come from the same place: search for printable strings, then match against substrings that are unique to the success and failure branches.

   The explore(find=..., avoid=...) method implements a directed search. Once a state reaches find, Z3 solves for the concrete input that satisfies all accumulated branch conditions. Limitations: path explosion on heavily branched code, slow on cryptographic operations or unbounded loops. Combine with concolic execution or targeted manual analysis when angr stalls.

Flag

Automated reverse engineering with angr or angr + symbolic execution quickly finds the valid input.