Level 0: Find the Backdoor Password

Welcome to symbolic execution! This binary reads a username and password from stdin. It tries to authenticate by opening a file named after the username and comparing the password to its contents - but this will fail unless the exact file exists on disk. However, there is a hardcoded backdoor password in the binary that bypasses this check entirely.

Use angr's symbolic execution to find the backdoor password. Symbolic execution will explore both code paths (file-based and backdoor) and find an input that reaches the success message without needing the file to exist.

When you find the input, extract ONLY the 8 bytes corresponding to the password (not the username). Decode it from bytes to a string and submit it.

Interesting APIs

• project.factory.entry_state() - create a state at the program's entry point
• project.factory.simulation_manager(state) - create a simulation manager
• simgr.explore(find=..., avoid=...) - run symbolic execution
• state.posix.dumps(0) - get concrete stdin bytes
• state.posix.dumps(1) - get concrete stdout bytes

Level 1: Stepping the Simulation Manager

Load the binary and create an entry_state. Wrap it in a simulation manager.

Step the simulation manager 8 times using simgr.step().

After stepping, submit the number of active states in the simulation manager.

The binary has multiple branching paths, so after enough steps the execution will have forked into multiple active states.

Interesting APIs

• project.factory.entry_state() - create initial state
• project.factory.simulation_manager(state) - wrap state in SimulationManager
• simgr.step() - advance all active states by one basic block
• simgr.active - list of currently active states
• len(simgr.active) - number of active states

Level 2: State Inspection - Resolve a String from Registers

The binary decodes an encoded string using XOR and reversal, then prints only its memory address via printf('The secret string is at: %p', secret_location). The actual string content is never printed.

Your task:

1. Use angr to explore to the printf call.
2. At the found state, read the rsi register which holds the second argument to printf (the %p pointer value).
3. Load the decoded string from memory at that address and resolve it.

Submit the resolved secret string.

Hint: rsi contains a pointer to the decoded string. Use state.memory.load(ptr, size) to read the bytes, then state.solver.eval(expr, cast_to=bytes) to concretize them.

Interesting APIs

• simgr.explore(find=addr) - explore to a specific address
• state.regs.rsi - read the RSI register
• state.memory.load(addr, size) - load bytes from memory
• state.solver.eval(expr, cast_to=bytes) - concretize a symbolic expression

Level 3: Constrained Symbolic Input

The binary reads 8 bytes of input and checks them through XOR operations. Without constraints, angr will return false positives - non-printable bytes or null characters that technically satisfy the check but are not valid passwords.

Your task:

1. Create symbolic bitvectors for the 8 input bytes
2. Add constraints so that all bytes are printable ASCII (0x20 to 0x7e)
3. Pass the constrained symbolic input when creating your initial state
4. Explore to find the "Access granted!" path
5. Submit the password string

Make sure all bytes of your input are constrained to be printable.

Interesting APIs

• claripy.BVS("name", 8) - create an 8-bit symbolic bitvector
• state.solver.add(byte >= 0x20) - add a constraint
• state.posix.dumps(1) - get concrete stdout
• simgr.explore(find=..., avoid=...) - symbolic exploration

Level 4: call_state - Calling a Function Directly

The binary has a validate_serial function that checks an 8-byte serial number. However, the program runs a heavy initialization routine before reaching the validation, making normal symbolic execution impractical.

Use factory.call_state() to call validate_serial directly, bypassing the expensive setup code. Pass a symbolic buffer as the argument.

The address of validate_serial can be found using the CFG/functions panel.

Submit the valid serial string. Constrain all bytes to printable ASCII.

Interesting APIs

• project.factory.call_state(addr, arg1, ...) - create state at a function entry
• angr.PointerWrapper(symbolic_buffer) - wrap a buffer so it's passed as a pointer
• claripy.BVS("name", 64) - create a 64-bit symbolic bitvector (8 bytes)
• simgr.explore(find=...) - explore to find the "return 1" path

Level 5: Hooking - Skip Expensive Code

The binary validates a serial number in two phases: validate_1 checks the first 4 bytes, then heavy_init runs an extremely expensive calibration loop, and finally validate_2 checks the last 4 bytes.

Running the binary normally (or with angr from entry_state) will hang on the heavy_init loop. The solution is to hook heavy_init so it returns immediately, then find the valid serial through symbolic execution.

What is hooking? Hooking replaces a function's implementation with your own. In angr, you can hook a symbol with a SimProcedure - a Python class that defines what the function should do during symbolic execution. For simple cases like skipping a function, angr provides built-in stubs like ReturnUnconstrained that just return without doing anything meaningful.

Interesting APIs

• project.hook_symbol('heavy_init', angr.SIM_PROCEDURES['stubs']['ReturnUnconstrained']())
• simgr.explore(find=..., avoid=...) - explore after hooking
• state.posix.dumps(0) - recover stdin

Level 6: Custom SimProcedure - Replacing an Obfuscated Function

The binary validates a serial using a deobfuscate(a, b) function. This function performs a real computation through an extremely convoluted path: slow nested loops, bit-by-bit extraction, repeated doubling with junk operations - and then hits a ud2 (undefined instruction) before it can return.

angr cannot execute past ud2, so symbolic execution will fail on every call to deobfuscate. Your task is to:

1. Reverse-engineer what deobfuscate(a, b) actually computes
2. Write a SimProcedure that implements the same logic cleanly
3. Hook the symbol and explore for the valid serial

Hint: strip away the noise and figure out what operations on a and b produce the final result.

Interesting APIs

• class MyProc(angr.SimProcedure): def run(self, a, b): ...
• project.hook_symbol('deobfuscate', MyProc())
• simgr.explore(find=..., avoid=...)
• state.posix.dumps(0) - recover stdin