Crossword

Platform: CUSTOM | Category: Reversing | Type: Challenge | Difficulty: Easy | OS: N/A | **Author: XESXOR Techniques: ascii_range_constraints, linear_diophantine_systems, reversed_operand_order, round_based_automation, rpn_evaluation, z3_constraint_solving

Summary

Walkthrough of the CUSTOM Reversing Crossword. Task: networked round-based challenge that feeds systems of Reverse Polish Notation equations whose variable values spell an ASCII string. Solution: parse RPN into z3 constraints, note the reversed-op

Description

Here are too weird crosswords. Can you solve? nc 109.233.56.90 11542

A remote service presents "crosswords" as systems of equations written in Reverse Polish Notation (RPN). Each unknown variable x1..xN represents one character of the answer string (its integer value is the ASCII code). Solve 11 rounds and the server returns the flag. A pwntools I/O template (crossword_template.py) was provided; only a process_equations(eqs) function had to be implemented. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Recon

Connecting interactively with nc reveals the protocol:

Welcome to Reverse Polish Crossword. Answer is string. For example, first is 'cat'.
Crossword 1 of 11, 3 equations:
99 x1 =
x2 2 1 * x1 - =
x3 9487 x1 x2 * - =

• There are 11 rounds ("Crossword K of 11, N equations:").
• Round K declares N equations and N unknown variables x1..xN.
• Each equation is a single RPN expression containing exactly one =, which acts as an equality constraint between the two sub-expressions on the stack.
• The answer is the string formed by interpreting each variable's integer value as an ASCII character (x1 → first char, etc.).
• Send the string back; after all 11 rounds are solved, the server prints the flag. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

The example round is supposed to spell cat (c=99, a=97, t=116).

Analysis

The key twist: reversed operand order

The RPN machine evaluates binary operators with reversed operand order. For a token sequence a b op, it computes b op a — not the standard a op b. This only matters for non-commutative operators (-, /), and it is exactly what the "cat" example forces:

• 99 x1 = → x1 = 99 = 'c' ✓
• x2 2 1 * x1 - = → the RHS is 2*1 x1 -, evaluated as x1 - (2*1) = 99 - 2 = 97 = 'a'. So x2 = 97.
• x3 9487 x1 x2 * - = → the RHS is (x1*x2) 9487 -, evaluated as (x1*x2) - 9487 = 99*97 - 9487 = 9603 - 9487 = 116 = 't'. So x3 = 116. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Result: cat. With naive/standard RPN order you instead get x2 = 2*1 - 99 = -97 and x3 = 9487 - 9603 = -19090, which do not spell anything printable. Reversing the operand order for binary ops fixes it.

Second pitfall: underdetermined systems / multiple integer solutions

Some rounds are linear systems that are underdetermined over the integers or admit several integer lattice points. z3 may return a valid-but-non-printable solution (a different lattice point than the intended letters). The fix is to constrain every variable to the printable-ASCII range 32 <= xi <= 126. With that bound z3 returns the intended readable string. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Importantly, the server accepts any valid printable-ASCII solution to the system — it does not require a single canonical answer — so the ASCII bound is sufficient to pass every round even when the intended word is ambiguous (e.g. round 2 came back as FR).

Solution

Use z3. Parse each RPN line token by token:

• numeric tokens → IntVal,
• x-tokens → z3 Int variables (created once, cached),
• binary operators → pop b then a, push the reversed operation b op a,
• = → pop the two stack ends and add an equality constraint a == b. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Then add 32 <= xi <= 126 for every variable, solve, sort variables by numeric index, and concatenate chr(value). Drive the 11-round loop with the provided pwntools template.

 python read-only • copy allowed Copy
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
import pwn
from z3 import *


def process_equations(eqs):
    s = Solver()
    vs = {}

    def getv(t):
        if t.lstrip('-').isdigit():
            return IntVal(int(t))
        if t not in vs:
            vs[t] = Int(t)
        return vs[t]

    for line in eqs:
        stack = []
        for tok in line.split():
            if tok == '=':
                b = stack.pop(); a = stack.pop(); s.add(a == b)
            elif tok in ('+', '-', '*', '/'):
                b = stack.pop(); a = stack.pop()
                # reversed operand order: compute b op a
                stack.append({'+': b + a, '-': b - a, '*': b * a, '/': b / a}[tok])
            else:
                stack.append(getv(tok))
    for v in vs.values():
        s.add(v >= 32, v <= 126)
    assert s.check() == sat, "unsat"
    m = s.model()
    out = ''
    for k in sorted(vs, key=lambda x: int(x[1:])):
        v = m[vs[k]].as_long()
        out += chr(v)
    return out
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍


def solve():
    r = pwn.remote('109.233.56.90', 11542)
    r.recvline()
    while True:
        line = r.recvline().decode().strip()
        print(line)
        if not line.startswith("Crossword"):
            print("FINAL:", line)
            return
        count = int(line.split()[4])
        lines = [r.recvline().decode().strip() for _ in range(count)]
        result = process_equations(lines)
        print("  ->", result)
        r.sendline(result.encode())


if __name__ == "__main__":
    solve()

‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Run evidence

The 11 solved answers were:

cat
FR          # linear system with multiple valid solutions
tgt
Ave.
thewy
Weider
vomiter
back-way
sugarings
Khoi-khoin
nose-leafed

followed by:

Gratz! spbctf{REDACTED}

The flag text itself is the hint the author intended: "z3 is too easy for me". ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Key Takeaways / Lessons

• Mastering ascii_range_constraints, linear_diophantine_systems, reversed_operand_order, round_based_automation, rpn_evaluation, z3_constraint_solving was key to this challenge.
• Always check for common misconfigurations and verify assumptions.

---

Crafted by XESXOR Research • 2026-07-02 • CUSTOM • Crossword • Difficulty: Easy