We are given an executable that expects 100 moves as input, where each move must be one of N, E, S, or W. There is no feedback whether a move is incorrect until all 100 moves are up. Alongside the executable, we are provided with a C function int alien_hash(char directions[]) that calculates a hash based on the sequence of moves.

The goal is to determine the correct sequence of moves that satisfies the hash check, and displays the flag. Brute forcing is computationally impossible, with a total of $4^{100}$ combinations. Since we need to find a sequence that satisfies a mathematical condition, we can approach this as a constraint solving problem, using an SMT solver like Z3.

What is Z3?

Z3 is an SMT Solver (Satisfiability Modulo Theory Solver), a type of theorem prover designed to determine whether a set of logical constraints can be satisfied.

Take the following example. Just as we need to find a sequence of moves that satisfies a hashing function, we can use Z3 to solve this problem:

# pip install z3-solver
from z3 import Solver, Int, sat
 
 
solver = Solver()
 
square = Int("square")
circle = Int("circle")
triangle = Int("triangle")
 
solver.add(square * square + circle == 16)
solver.add(triangle * triangle * triangle == 27)
solver.add(triangle * square == 6)
 
if solver.check() == sat:
    model = solver.model()
 
    square_val = model.eval(square).as_long()
    circle_val = model.eval(circle).as_long()
    triangle_val = model.eval(triangle).as_long()
    product = square_val * circle_val * triangle_val
 
    print("Found Solution!")
    print(f"Square:   {square_val}")
    print(f"Circle:   {circle_val}")
    print(f"Triangle: {triangle_val}")
    print(f"Product:  {product}")
else:
    print("No solution found.")
 
# Found Solution!
# Square:   2
# Circle:   12
# Triangle: 3
# Square * Circle * Triangle = 72

This is similar to our challenge: we define unknown values (our move sequence), express mathematical constraints on them, and let Z3 compute valid values that satisfy those constraints.

Replicating C's Hashing Functionality

The first step was to accurately replicate the C alien_hash function in both Python and Z3.

In the C program, different data types are used:

• Directions: 100 × 1 byte (char[100]) → Stores the 100-step sequence of moves.
• Hash: 37 × 1 byte (char[37]) → Stores the computed hash value.
• Checksums: 3 × 4 bytes (int[3]) → Used for verification.

Understanding C's Arithmetic Behavior

When performing arithmetic operations on mixed data types, C promotes smaller types (such as char) to a 32-bit or 64-bit register for computation. After the calculation, the result is truncated to fit back into the intended storage size.

Python, however, uses arbitrary precision, so values don't overflow naturally. To match C's behaviour when storing into char hash[i], we can perform all calculations in Python's larger bit space and then extract the lower 8 bits at the end.

It's important to note that signed and unsigned integers are just two interpretations of the same byte. In this challenge hash[i] is only written to and unused in further calculations (only compared as bytes), so the signedness is irrelevant.

Another key difference is C automatically performs integer division when operands are integers, whereas Python defaults to floating-point division. To fully replicate the C program's behaviour, we must explicitly use integer division in Python.

Matching C's behaviour in Python:

1. Use integer division (//).
2. Truncate values to 8-bit integers when storing using a 0xFF mask.

Matching C's behaviour in Z3:

1. Use BitVec(..., 32) (32-bit values) for all types.
   1. Supports Bitwise operations.
   2. Already uses integer division.
   3. Simulates C's promotion to int / larger bit space, preventing premature wrapping.
2. Truncate values to 8-bit integers when storing using Extract(7, 0, ...).

Solving

Now that we understand what is required to replicate the C alien_hash function, we can define the constraints in Z3.

from z3 import Solver, BitVecVal, Extract
 
# Initialise Solver
# Define 100 directional inputs
# Define Valid Movements (N, E, S, W)
# Define Expected Hash Values
hash_values = [BitVecVal(ord(c), 8) for c in desired_hash]
 
# Modulo constraints
# Checksum constraints
# Hash value & computation constraints
# ...
solver.add(hash_values[0] == ((directions[6] ^ directions[10]) & 0xF)  +  ((directions[3] + directions[5] - 25 ) ^ (3*directions[99])))
solver.add(hash_values[1] == Extract(7, 0, ...))
solver.add(hash_values[2] == Extract(7, 0, ...))
solver.add(hash_values[3] == Extract(7, 0, ...))
# ...

With the constraints defined, Z3 returns a valid sequence of moves that satisfies all conditions.

Instead of manually typing the 100 moves into the challenge executable, I wrote a small script to pipe the solved path in automatically, passing the hash check and printing the flag!

When I revisited this challenge, I realised my original solver did not model the char assignment step. In C, each hash[i] is computed in a wider bit-space and then truncated to 8 bits when stored.

Applying truncation causes values to wrap into the 0-255 range, increasing potential solutions. I modified the solver to add a blocking constraint after each solution so Z3 would find all possible paths.

The solver now finds all 30 solutions!

I've also just noticed, every successful flag is in the format BLK-BOX{...}, and the contents are an md5 hash of the correct path. Just something I noticed and found interesting!