← Back to Writeups
CUSTOMMediumReversing
Bookmark

Mips Mops

XESXOR9/10/20268 min read
#reversing#custom#medium#forward_model_reconstruction#ground_truth_validation#pairwise_equation_solving#static_disassembly#uninitialized_stack_resolution#z3_inversion#linux

Mips Mops

Platform: spbctf | Category: Reversing | Type: Challenge | Difficulty: Medium | OS: Linux | Author: XESXOR | Date: 2026-07-02 | Status: Solved Techniques: forward_model_reconstruction, ground_truth_validation, pairwise_equation_solving, static_disassembly, uninitialized_stack_resolution, z3_inversion

Summary

Task: stripped MIPSEL PIE keygen validating a 32-char serial; the flag IS the correct serial. Solution: statically reverse the 64-bit-on-32-bit transform (fixing a compiler-emitted word-swapped multiply constant), build a Python forward model validated against qemu-user, then invert the check with z3 and pairwise equation solving, resolving an uninitialized A[7] stack slot via surrounding readable text.

Mips Mops — spbctf

Description

Do you like dogs? How about mops? How about mips?

apt -y install qemu-user-static libc6-mipsel-cross
qemu-mipsel -L /usr/mipsel-linux-gnu ./mips_mops.elf <serial>

We are given mips_mops.elf, a stripped 32-bit MIPSEL PIE keygen. It takes a 32-character serial as argv[1] and, on success, prints [+] Serial is correct! Your flag is: %s where the %s is the serial itself. The flag IS the correct serial — solving the keygen recovers it directly. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

Analysis

Recon

$ file mips_mops.elf
ELF 32-bit LSB pie executable, MIPS, MIPS32 rel2, dynamically linked,
interpreter /lib/ld.so.1, stripped, BuildID=774af042d235b1a5b3b1bda804333072fa258d8f

Strings expose the keygen flow: [*] USAGE: %s serial_number, [*] Checking serial..., [-] Wrong length!, [-] Bad characters in serial, [-] No., plus a large ASCII-art pug ("mops").

The transform (main @ file offset 0x7f0)

An 8-entry array A of uint64 lives at fp+0x30 (little-endian word pairs); the serial pointer is at fp+0x28. The check is: ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

  1. Length: strlen(serial) == 0x20 else Wrong length!.
  2. Charset: every byte 0x20 <= c < 0x7f else Bad characters in serial.
  3. Init A[idx] for idx = 0..6 (note the loop is slti ...,7, so A[7] is never initialized — see the subtlety below):
    • n = idx + 1
    • s1 = (n*0x0101010101010101 + 0x6efec0b2c164718f) mod 2^64
    • s2 = rotr64(s1, 37) (asm renders this as a word-swapped "rotr by 5")
    • mult = (idx*0x4ba299375e3615c1 + 0x5b867ed88b434e15) mod 2^64
    • A[idx] = (s2 * mult) mod 2^64
  4. k-loop, k = 0..31: A[k%8] = rotr64(A[k%8] XOR serial[31-k], 40) (word-swapped "rotr by 8"). The serial is absorbed in reverse index order.
  5. Finalize each slot with a per-slot add/xor of a 64-bit constant (see FIN in the model).
  6. Compute 16 output words B from the 4 pairs (P=A[2m], Q=A[2m+1], all 32-bit halves):
    • B[4m+0] = Phi + Qlo
    • B[4m+1] = Plo - Qhi
    • B[4m+2] = Plo + Qhi
    • B[4m+3] = Phi - Qlo (all mod 2^32)
  7. Final check: B[i] + const_i == 0 for all 16 i, i.e. B[i] == (-const_i) mod 2^32. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

The bug that broke the naive model — word-swapped multiply constant

The single biggest trap: in step 3 the multiply constant is 0x4ba299375e3615c1, which is K1 = 0x5e3615c14ba29937 with its two 32-bit halves swapped. This swap is an artifact of how the compiler expanded a 64-bit multiply of the small integer idx by the constant on 32-bit MIPS:

mul $v1,$s3,0x5e3615c1
mul $v0,$s2,0x4ba29937   ; cross terms of the 64-bit product

A naive model that used 0x5e3615c14ba29937 directly produced wrong A values and never matched the ground truth. Only after decoding the exact instruction sequence with capstone and reproducing the cross-term expansion did the forward model agree with qemu. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

The A[7] uninitialized-stack subtlety

A[7] is used in the k-loop (k = 7,15,23,31 → slot 7) and in pair m=3 (B[12..15]), yet it is never written by the init loop. On a real Linux process the initial stack is zero-filled, so the intended A[7] = 0. Under qemu-user invoked via the dynamic loader, that stack slot holds leftover loader garbage (observed 0x3ffffc7040048000), which is why running the real binary under qemu printed No. even for the correct flag. The four flag bytes fed by slot 7 are serial[0], serial[8], serial[16], serial[24] (positions 0, 8, 16, 24). ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

Solution

Narrative: recon → static RE of the transform → Python forward model → validation against qemu ground truth → discovery of the swapped-constant bug → z3 inversion → resolving the A[7] ambiguity via readable text → verification.

Corrected forward model

 python 
#!/usr/bin/env python3
# CORRECTED forward model of mips_mops.elf serial check (verified vs qemu)
M64 = (1 << 64) - 1
M32 = (1 << 32) - 1

def rotr64(x, n):
    x &= M64
    return ((x >> n) | (x << (64 - n))) & M64

C1   = 0x0101010101010101
ADD1 = 0x6efec0b2c164718f
K1s  = 0x4ba299375e3615c1   # word-SWAPPED K1 (the crucial bug fix)
K2   = 0x5b867ed88b434e15
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

def init_A(a7=0):
    A = [0] * 8
    for idx in range(7):          # slti ...,7  -> A[7] left uninitialized
        n    = idx + 1
        s1   = (n * C1 + ADD1) & M64
        s2   = rotr64(s1, 37)
        mult = (idx * K1s + K2) & M64
        A[idx] = (s2 * mult) & M64
    A[7] = a7                      # intended value is 0 (zeroed stack)
    return A

def kloop(A, serial):
    A = A[:]
    for k in range(32):
        A[k % 8] = rotr64(A[k % 8] ^ serial[31 - k], 40)
    return A

FIN = [('+', 0x2d2307d7e9a1fa83), ('^', 0xe887f2d23433c7d6),
       ('+', 0x572c1d4bf123b0b7), ('+', 0x8f138e135a7ac1fd),
       ('^', 0x6c107ff75570821a), ('+', 0x28ddb3b8fb191d0f),
       ('+', 0x33330da68ea7cacd), ('^', 0xea4d2d5c43f59642)]
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

def finalize(A):
    A = A[:]
    for i, (o, c) in enumerate(FIN):
        A[i] = (A[i] + c) & M64 if o == '+' else A[i] ^ c
    return A

def compute_B(A):
    B = [0] * 16
    for m in range(4):
        P, Q = A[2 * m], A[2 * m + 1]
        Plo, Phi = P & M32, (P >> 32) & M32
        Qlo, Qhi = Q & M32, (Q >> 32) & M32
        B[4 * m]     = (Phi + Qlo) & M32
        B[4 * m + 1] = (Plo - Qhi) & M32
        B[4 * m + 2] = (Plo + Qhi) & M32
        B[4 * m + 3] = (Phi - Qlo) & M32
    return B

def full_forward(serial, a7=0):
    return compute_B(finalize(kloop(init_A(a7), serial)))
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

consts = [0xe70fe185, 0xc8729904, 0x245f0ca6, 0x145a73f3,
          0x90c30f85, 0x2aa087ee, 0xdae0dc24, 0x1ec0a50d,
          0xdb4a13ab, 0x1007bac8, 0x4ab83c5c, 0x2b7ed257,
          0x88b96c6e, 0x3464f8fb, 0x60209ee7, 0xeaa55af2]
TARGET = [(-c) & M32 for c in consts]

def unfinalize(A):
    A = A[:]
    for i, (o, c) in enumerate(FIN):
        A[i] = (A[i] - c) & M64 if o == '+' else A[i] ^ c
    return A

z3-based inverse solver

 python 
import itertools
from z3 import BitVec, BitVecVal, RotateRight, ZeroExt, Solver, sat
from model import (M32, TARGET, unfinalize, init_A, full_forward)
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

def solve_2x(v):
    # solve 2*x == v (mod 2^32); v must be even, two roots
    v &= M32
    if v & 1:
        return []
    h = v >> 1
    return [h, (h + (1 << 31)) & M32]

def recover_A_fin():
    # invert compute_B pairwise: B0,B3 -> 2*Phi, 2*Qlo ; B1,B2 -> 2*Plo, 2*Qhi
    cp = []
    for m in range(4):
        B0, B1, B2, B3 = TARGET[4 * m:4 * m + 4]
        opts = []
        for Phi in solve_2x((B0 + B3) & M32):
            for Qlo in solve_2x((B0 - B3) & M32):
                if (Phi + Qlo) & M32 != B0 or (Phi - Qlo) & M32 != B3:
                    continue
                for Plo in solve_2x((B2 + B1) & M32):
                    for Qhi in solve_2x((B2 - B1) & M32):
                        if (Plo - Qhi) & M32 != B1 or (Plo + Qhi) & M32 != B2:
                            continue
                        opts.append(((Phi << 32) | Plo, (Qhi << 32) | Qlo))
        cp.append(opts)
    res = []
    for c in itertools.product(*cp):
        A = [0] * 8
        for m in range(4):
            A[2 * m], A[2 * m + 1] = c[m]
        res.append(A)
    return res
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

def invert_slot(S_i, E_i):
    # 4 bytes b s.t. chaining rotr64(st ^ b, 40) from init S_i reaches E_i
    s = Solver()
    bs = [BitVec(f'b{k}', 8) for k in range(4)]
    st = BitVecVal(S_i, 64)
    for n in range(4):
        st = RotateRight(st ^ ZeroExt(56, bs[n]), 40)
    s.add(st == BitVecVal(E_i, 64))
    if s.check() == sat:
        m = s.model()
        return [m[bs[n]].as_long() for n in range(4)]
    return None

for A_fin in recover_A_fin():
    A_afterk = unfinalize(A_fin)
    S = init_A()                      # S[7] = 0 (intended)
    serial = [None] * 32
    ok = True
    for i in range(8):
        b = invert_slot(S[i], A_afterk[i])
        if b is None:
            ok = False
            break
        for n in range(4):
            serial[31 - (i + 8 * n)] = b[n]
    if not ok:
        continue
    s = bytes(serial)
    if full_forward(s) == TARGET:
        print(repr(s))

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

Slots 0..6 have deterministic init, so all 28 of their bytes solve uniquely to printable ASCII. Slot 7's four bytes depend on the unknown A[7] init, but the surrounding readable text pinned them: .pbctf{y.ur_seri.l_is_LO.E_mips} → s, o, a, V → spbctf{REDACTED}.

Verification: full_forward(flag, a7=0) == TARGET exactly, and patching A[7]=0 in gdb makes the real binary print [+] Serial is correct! Your flag is: spbctf{REDACTED}.

Ground-truth / environment tips

  • Static analysis: radare2 (aaa, pdf) + capstone for exact decoding of the 64-bit-arithmetic-on-32-bit-MIPS expansion (this is how the swapped constant was caught).
  • Ground truth: qemu-user-static + libc6-mipsel-cross inside a Docker debian:bookworm-slim --platform linux/amd64 container. macOS has no native qemu-user.
  • qemu could not auto-load the PIE (rc=1, no syscalls under -strace). Workaround — invoke the dynamic loader explicitly: qemu-mipsel-static -L /usr/mipsel-linux-gnu /usr/mipsel-linux-gnu/lib/ld.so.1 ./mips_mops.elf ARG.
  • Under that invocation the PIE base was 0x3f7e0000 (found via -d page: the small 2-page r-x region that isn't ld.so@0x40000000 or libc@0x3f5f0000). Breakpoint at check = base+0x12f4; read B at $s8+0x70, A at $s8+0x30, serial ptr at [$s8+0x28]. The qemu MIPS gdbstub does not populate $fp in gdb-multiarch — use $s8; syscall catchpoints are unsupported.
  • Unicorn pitfall: its MIPS mode mis-models the historical load-delay slot for consecutive lw (value appears one instruction late), making it unusable here.
  • binfmt pitfall: multiarch/qemu-user-static --reset -p yes can register qemu as the interpreter for the host arch too and break normal amd64 container execution; a Docker VM restart clears the binfmt_misc state. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍