Path exploration using Angr - Björn CTF 2025

Last week I participated to Björn CTF, which was a CTF organized by my team and that’s where I encountered a challenge that initially appeared impossible to solve through conventional means. However, by leveraging the Angr framework for symbolic execution and path exploration, I was able to uncover the solution.

Rev

House of 1000 conditions

So many branches, so little sanity. Only automation can survive this house.

We are given a binary and first thing I tried is to decompile it with Ghidra. But the decompiled code just shis just a mess of nested if statements checking for specific values in an array and if all conditions are met, we are prompted with “the doors realign for your auto mation. you stagger out, victorious.” and otherwise “the house rearranges its corridors around you. sanity erodes.”. Unfortunately, checking all the conditions manually is not feasible, but from the decompiled code we can still see some useful information:

  if (param_1 < 2) {
    puts("the house snarls: offer your incantation as an argument.");
  }
  else {
    __s = *(byte **)(param_2 + 8);
    sVar310 = strlen((char *)__s);
    if (sVar310 == 0x33) {

From this snippet we can see that the input is expected as a command line argument and that the length of the input should be 0x33 (51), otherwise we will not pass the first 2 checks.

Knowing this, we can now use Angr to explore the different paths in the binary and find the correct input that will lead us to the victorious message.

To do this, we can create a symbolic variable for the input with length 51 bytes and set up the initial state of the program which takes this symbolic input as an argument. We can also add constraints to ensure that the input consists of printable ASCII characters only and more importantly, we can instruct Angr not to check satisfiability of every path immediately, but instead to delay this until we find a path that leads to our goal. This is important because the binary has a huge number of branches and checking satisfiability for every path would be computationally expensive, so we use the angr.options.LAZY_SOLVES option to delay this process.

The following code demonstrates how to set up Angr for this challenge and explore the paths to find the correct input:

import angr
import claripy

FLAG_LENGTH = 51            # Length of the input flag

FIND = b"victorious"        # Message indicating success
AVOID = b"sanity erodes"    # Message indicating failure

proj = angr.Project('house', auto_load_libs=False)
flag = claripy.BVS("flag", FLAG_LENGTH * 8)

state = proj.factory.full_init_state(
        args=[proj.filename, flag],
        add_options={
            angr.options.LAZY_SOLVES,                       # Avoid satisfiability checks until necessary
            angr.options.ZERO_FILL_UNCONSTRAINED_MEMORY,    # Suppress warnings
            angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS  # Suppress warnings
        }
)

for i in range(FLAG_LENGTH):
    byte = flag.get_byte(i)
    state.solver.add(byte >= 0x20, byte <= 0x7E)            # Constrain every byte to be printable ASCII

simgr = proj.factory.simgr(state)
simgr.explore(
    find=lambda s: FIND in s.posix.dumps(1),
    avoid=lambda s: AVOID in s.posix.dumps(1)
)

if not simgr.found:
    print("No path")
else:
    model = simgr.found[0].solver
    solution = model.eval(flag, cast_to=bytes)
    print(solution.decode())

Flag: flagbot{symb0lic4lly_3xorc1s3d_th3_1000_cond1t10ns}