SMS Server

Platform: spbctf | Category: Reversing | Type: Challenge | Difficulty: Medium | OS: Windows | Author: XESXOR | Date: 2026-07-02 | Status: Solved Techniques: equation_extraction_from_disasm, static_disassembly, string_xref_analysis, uniqueness_proof, z3_constraint_solving

Summary

Task: Windows Lazarus/FPC GUI crackme (smsserver.exe) validates a 30-char serial via 60 quadratic constraints of the form (s[i]*s[j]) XOR (s[k]*s[l]) == const embedded as lea rax,[rax-C]. Solution: extract all equations from radare2 disassembly with a symbolic register tracker, feed them to z3 as 32-bit BitVecs with printable-ASCII bounds, solve for the unique serial.

SMS Server — spbctf

Description

SMS Server — validate the serial in the txtSerial field to register the application.

A Windows GUI crackme (smsserver.exe). Enter a serial into the txtSerial field; the correct serial makes the app show "Congratulations! The serial is correct" and switch to the "Registered" state. Goal: recover the correct serial, which is itself the flag.

Analysis

Recon

$ file smsserver.exe
smsserver.exe: PE32+ executable (GUI) x86-64, for MS Windows   (~2.8 MB)

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

strings shows this is a Lazarus / Free Pascal application:

FPC 3.0.4 [2020/04/11] for x86_64 - Win64
LCL... (Lazarus Component Library class names)
txtSerial
Serial Correct
Congratulations!\n\nThe serial is correct
Registered
Bad serial
Error

The interesting strings live in .rdata:

Locating the check

Using radare2 (aaa), axt on those string VAs points to the button OnClick handler at 0x10002bd50:

1. Reads txtSerial into an AnsiString (call @ 0x10002bd88).
2. Calls the validator @ 0x10002bca0.
3. If AL != 0 → MessageBox "Serial Correct" / "Congratulations!", sets caption/status to "Registered". Otherwise → "Error" / "Bad serial".

Validator @ 0x10002bca0

cmp rax, 0x1e        ; AnsiString length (from [ptr-8]) must equal 30

The validator enforces len == 30 and then calls four boolean sub-check functions; all must return true (test al,al; jne chains), otherwise the result is 0: ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

0x10002afa0   (F1)
0x10002b3f0   (F2)
0x10002b7d0   (F3)
0x10002b9f0   (F4)

Returns 1 only if length == 30 AND all four sub-checks pass.

The equation system

Each sub-check is a sequence of independent constraints. Every constraint has this exact assembly shape:

 asm read-only • copy allowed Copy
movzx eax, byte [ptr + i]    ; load serial[i]
movzx edx, byte [ptr + j]    ; load serial[j]
imul  rax, rdx               ; A = s[i]*s[j]
movzx ..., byte [ptr + k]
movzx ..., byte [ptr + l]
imul  ...                    ; B = s[k]*s[l]
xor   rax, rB                ; A ^ B
lea   rax, [rax - CONST]     ; subtract embedded constant
test  rax, rax
jne   fail                   ; must be zero  ->  (A ^ B) == CONST

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

So each constraint is:

(s[i] * s[j]) XOR (s[k] * s[l]) == CONST

where CONST is the immediate in the lea rax, [rax - CONST]. There are 60 such equations across the four functions, over the 30 serial bytes.

Sample equations (60 total):

(s[4]*s[20])  ^ (s[28]*s[10]) == 0x1f3c
(s[22]*s[25]) ^ (s[16]*s[3])  == 0x2b1
(s[9]*s[18])  ^ (s[0]*s[17])  == 0x4cb
(s[28]*s[9])  ^ (s[9]*s[8])   == 0x7c8
(s[18]*s[14]) ^ (s[6]*s[5])   == 0x5ba
...

Solution

Extracting the equations reliably

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

radare2's default disassembly prints box-drawing flow arrows that break naive address/line regexes. Disable the decoration before dumping each function:

e scr.color=0
e asm.lines=false
e asm.bytes=false
e asm.comments=false
s <func>
pD <size>

Respect exact function boundaries so pD does not bleed into the next function:

F1  0x10002afa0 .. 0x10002b3f0
F2  0x10002b3f0 .. 0x10002b7d0
F3  0x10002b7d0 .. 0x10002b9f0
F4  0x10002b9f0 .. 0x10002bc72

A small symbolic tracker maps registers/stack-slots to expressions: ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

• movzx R, byte [ptr+idx] → R = ('b', idx)
• imul R, S → R = ('p', R, S) (product)
• xor R, S → R = ('x', R, S)
• lea R, [R - C] → emit equation expr_of(R) == C

Pitfall: 7 spurious "equations" with constants 0x20 / 0x60 / 0x70 / 0x90 / 0xa0 are just function-prologue lea rsp, [rsp-0xNN] stack adjustments. Filter those (they target rsp) → net 60 real equations.

Solving with z3

• 30 serial bytes as 32-bit BitVecs (products reach 127*127 = 16129; 32-bit width avoids overflow during imul/xor).
• Bound each byte to printable ASCII: 0x20 <= s[i] <= 0x7e.
• Add all 60 equations (s[i]*s[j]) ^ (s[k]*s[l]) == CONST.
• check() → sat. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

 python read-only • copy allowed Copy
#!/usr/bin/env python3
# Solve the SMS Server crackme serial with z3.
import json
from z3 import BitVec, Solver, sat, Or

# eqs.json: list of [expr_tree, CONST], where expr_tree is a nested list:
#   ["b", idx]                 -> serial byte idx
#   ["p", a, b]                -> a * b
#   ["x", a, b]                -> a ^ b
# (One leading garbage entry from an rsp prologue is filtered by rsp targets;
#  here we simply skip any entry whose expr tree is not a valid xor-of-products.)
EQS = json.load(open("eqs.json"))
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

s = [BitVec(f"s{i}", 32) for i in range(30)]

def build(node):
    tag = node[0]
    if tag == "b":
        return s[node[1]]
    if tag == "p":
        return build(node[1]) * build(node[2])
    if tag == "x":
        return build(node[1]) ^ build(node[2])
    raise ValueError(node)

solver = Solver()
for i in range(30):
    solver.add(s[i] >= 0x20, s[i] <= 0x7e)   # printable ASCII

count = 0
for expr, const in EQS:
    if expr[0] != "x":       # skip prologue-noise / non-constraint entries
        continue
    solver.add(build(expr) == const)
    count += 1
assert count == 60, count
‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

assert solver.check() == sat
m = solver.model()
serial = bytes(m[s[i]].as_long() & 0xff for i in range(30)).decode()
print("SERIAL:", serial)

# Prove uniqueness: forbid the found model and re-check.
solver.add(Or([s[i] != (m[s[i]].as_long()) for i in range(30)]))
print("unique:", solver.check() != sat)

Output:

SERIAL: REDACTED
unique: True

The model decodes to exactly 30 printable characters. Adding a Or([s[i] != found[i]]) clause and re-running gives unsat, proving the serial is the unique printable solution. Plugging it back into all 60 equations satisfies every one. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍

Entering REDACTED into txtSerial shows "Congratulations! The serial is correct" and the app becomes "Registered".

Semantic note

The serial is a self-referential hint: 4NGR3D = angr / z3 constraint-solver challenge, SER1AL = serial. It is designed to be solved by a solver, not by hand. ‍​‌‌​​​​‌​‌‌​​‌‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​‌‌​​‌‌​​‌‌​​‌​‌​‌‌​​‌​‌‍