Writeup: Wasmbler - upCTF (Reverse)

Overview

The challenge presents a web page at http://46.225.117.62:30023 with an input field for the flag. Validation is performed entirely client-side using WebAssembly (WASM) via the exported check_flag function.

<script src="challenge.js"></script>
<script>
  function go() {
    const v = document.getElementById('fi').value.trim();
    const ok = Module.ccall('check_flag', 'number', ['string'], [v]);
    // ok = 1 → correct, 0 → wrong
  }
</script>

Analysis

1. Download & Disassemble the WASM

curl -s http://46.225.117.62:30023/challenge.wasm -o challenge.wasm
wasm2wat challenge.wasm

The WASM file is 3584 bytes, compiled from C using Emscripten.

2. VM Architecture

Inside the WASM binary lies a custom bytecode VM with the following memory layout:

3. Instruction Set (13 operations)

4. Anti-Analysis: Function Table Shuffle

The key trick that makes this challenge interesting: after every single instruction, the function dispatch table is shuffled using a Fisher-Yates shuffle driven by an LCG PRNG.

seed = (seed * 1103515245 + 12345) & 0x7FFFFFFF

This means bytecode value 0x05 could map to a completely different operation at each execution step, depending on the current PRNG state. This makes static analysis without simulation impossible — you must faithfully replay the shuffle to know which operation each bytecode byte actually performs.

5. check_flag Flow (func 17)

1. Check strlen(input) == 38, return 0 if not
2. Copy function table template to working area
3. Set input pointer
4. Loop: while PC < 387:
     a. Read bytecode[PC], increment PC
     b. opcode = byte % 13
     c. Lookup func_table[opcode] → func_idx
     d. Execute operation based on func_idx
     e. Shuffle function table (Fisher-Yates + LCG)
5. Return pop() → must be 1 for correct flag

6. Constraint Pattern

By tracing execution, a repeating pattern emerges for each flag character:

PUSH_IMM <index>        ; character index
LOAD_INPUT              ; load flag[index]
<transform ops>         ; ROL/ROR/XOR/ADD/SUB/SHL/SHR/etc.
PUSH_IMM <expected>     ; expected value after transformation
EQ                      ; compare
AND                     ; accumulate into running result

Some constraints involve 2-3 characters at once (e.g., flag[a] XOR flag[b] == constant), creating cross-character dependencies.

Solver

The solver uses symbolic execution with Z3 — running the VM symbolically where each flag[i] is a Z3 BitVec variable, then solving all constraints simultaneously.

from z3 import *

flag = [BitVec(f'f{i}', 8) for i in range(38)]

# Simulate VM symbolically, collecting constraints
# (see solve2.py for full implementation)

# Key operations handled symbolically:
# - PUSH_IMM: push concrete BitVecVal
# - LOAD_INPUT: push symbolic flag[index]
# - ADD/SUB/XOR/OR/AND/SHL/SHR/ROL/ROR/MOD: Z3 bitvector ops
# - EQ: If(a == b, 1, 0)
# - AND: accumulate results

solver = Solver()
solver.add(result == BitVecVal(1, 8))

# Format constraints
solver.add(flag[0] == ord('u'))
solver.add(flag[1] == ord('p'))
# ... etc

if solver.check() == sat:
    m = solver.model()
    print(''.join(chr(m[flag[i]].as_long()) for i in range(38)))

Verification

$ python3 solve2.py
Solving...
Flag: upCTF{n3rd_squ4d_4ss3mbl3_c0de_7f2b1d}

$ python3 verify.py  # concrete VM execution
VM check result: 1 (PASS)

Tools

• curl — download the WASM binary
• wabt (wasm2wat) — disassemble WASM to WAT text format
• Python + Z3 — symbolic execution & constraint solving

Flag

upCTF{n3rd_squ4d_4ss3mbl3_c0de_7f2b1d}