Indirect Memory Access — b01lers CTF

Description

Original challenge statement was not preserved in the workspace.

Files provided:

• chal.gba — the Game Boy Advance ROM.

The ROM prints Press Button: in a loop, emits characters from the alphabet absSRLUDrl, collects 128 inputs, and on success prints flag is 'bctf{<above chars>}'. The goal is to recover the exact accepted input sequence and decode the resulting flag contents.

Analysis

The obvious starting point is the main loop near 0x080015b4. It prompts for one button at a time, stores a per-step value in IWRAM near 0x030000a0, increments a counter at 0x0300009c, and after 0x80 iterations calls the validator at 0x08000310.

The ROM also contains the lookup string:

absSRLUDrl

At first glance the challenge looks like it may care about the full ten-button GBA input alphabet. The key reversing insight is that the validator at 0x08000310 does not preserve that full semantics. The meaningful state per position is only one bit:

• A button → 1
• any non-A button → 0

So the real problem is not a ten-symbol input alphabet but a hidden 128-bit boolean constraint system.

The hard part is that a naïve static model is wrong. The validator at 0x08000310 relies on helper code copied into IWRAM around 0x03000025, and that helper's behavior changes depending on DMA3 state. During validation, DMA3 rewrites its source blob from several small ROM tables, so the same-looking call site can execute a different boolean gate at runtime. Static disassembly of the ROM therefore misses the exact logic that is actually checked.

To recover the real behavior, I used mGBA's GDB remote stub and traced:

• calls into the runtime-copied IWRAM helper,
• the active DMA3 source address for each call,
• how helper outputs changed under controlled inputs.

That showed a small family of exact boolean gates selected by the current DMA3 source blob. Correct modeling required following the actually executed validator path instead of the intended-looking ROM logic: in total, the successful reconstruction contained 450 helper calls. Once the executed path and gate type for each call were reconstructed, the validator reduced cleanly to an exact 450-gate boolean circuit over 128 input bits.

The final layer is an encoding trick: the valid bitstring is interpreted as unary runs over the alphabet absSRLUDrl. A 1 terminates a run of zeros, and the zero count selects the corresponding character from the lookup string. Solving the circuit therefore yields both the accepted button pattern and the decoded text inside the flag.

Solution

Step 1 — identify the real input domain

Tracing the input handling shows that although many buttons appear available, validation only distinguishes between A and not-A. That collapses the problem to 128 boolean variables.

Step 2 — trace runtime helper behavior

The validator calls a helper copied into IWRAM near 0x03000025. Because DMA3 rewrites the source blob during execution, static lifting of the ROM code is misleading and initially leads to the wrong model. I used mGBA + GDB to log the helper calls and correlate each one with the current DMA3 source address.

Step 3 — reconstruct the boolean circuit

Each active DMA3 source blob corresponded to one exact boolean gate behavior. Rebuilding the exact executed path produced 450 helper invocations, which in turn gave an exact 450-gate circuit whose inputs are the 128 per-step bits and whose final output is the validator success bit.

Step 4 — solve and decode

I modeled the recovered circuit in Z3, added the unary-run constraints required by the absSRLUDrl decoding, and solved for a satisfying 128-bit sequence. Decoding that bitstring produced:

aSbaabababaaabbasaaSbsaaaasLaRRbaaDaaaaDbRaabasaRaabsbSabas

which gives the final flag:

bctf{aSbaabababaaabbasaaSbsaaaasLaRRbaaDaaaaDbRaabasaRaabsbSabas}

Solve script

#!/usr/bin/env python3
import json
from pathlib import Path
from z3 import And, Bool, BoolVal, If, Not, Or, Solver, sat

MAPPING = "absSRLUDrl"


def row_expr(a, b, t00, t10, t01, t11):
    rows = []
    if t00:
        rows.append(And(Not(a), Not(b)))
    if t10:
        rows.append(And(a, Not(b)))
    if t01:
        rows.append(And(Not(a), b))
    if t11:
        rows.append(And(a, b))
    return BoolVal(False) if not rows else Or(*rows)


def decode(bits):
    out = []
    z = 0
    for bit in bits:
        if not bit:
            z += 1
        else:
            out.append(MAPPING[z])
            z = 0
    if z != 0:
        raise ValueError("trailing zeros")
    return "".join(out)


def main():
    circuit = json.loads(Path("circuit.json").read_text())
    cols = json.loads(Path("call_columns.json").read_text())
    const_beh = json.loads(Path("const_call_behaviors.json").read_text())

    n_inputs = 128
    xs = [Bool(f"x{i}") for i in range(n_inputs)]
    nodes = []

    def ref(r):
        kind, val = r
        if kind == "in":
            return xs[val]
        if kind == "node":
            return nodes[val]
        if kind == "const":
            return BoolVal(bool(val & 0xFFFF))
        raise ValueError(r)

    for i, call in enumerate(circuit["calls"]):
        a = ref(call["a"])
        b = ref(call["b"])
        key = str(i)
        if key in const_beh:
            beh = const_beh[key]
            if beh["kind"] in ("const_a", "const_b"):
                expr = If(
                    b if beh["kind"] == "const_a" else a,
                    BoolVal(bool(beh["out1"])),
                    BoolVal(bool(beh["out0"])),
                )
            else:
                raise ValueError(beh)
        else:
            expr = row_expr(a, b, cols["00"][i], cols["10"][i], cols["01"][i], cols["11"][i])
        nodes.append(expr)

    s = Solver()
    s.add(xs[-1])
    for i in range(n_inputs - 9):
        s.add(Or(*xs[i : i + 10]))

    s.add(nodes[circuit["final_node"]])

    if s.check() != sat:
        print("unsat")
        return

    m = s.model()
    bits = [bool(m.eval(x, model_completion=True)) for x in xs]
    seq = decode(bits)
    print(seq)
    print(f"bctf{{{seq}}}")


if __name__ == "__main__":
    main()