articleAug 14, 2020
SharkyCTF z3z3 — constraint-solving RE theme
High-level note on SharkyCTF z3z3: a reverse challenge whose flag check is a large pile of byte constraints, intended to be modeled with an SMT solver. Solve steps and PoC omitted.
SharkyCTF z3z3 (high-level)
What it is. SharkyCTF reverse-engineering challenge themed around Z3 / SMT solving (z3z3).
Challenge theme.
- Binary reads a short input (
fgets-scale length) - Wrong guesses print a playful
3Z Z3 z3…style message - A
check_flagpath encodes many arithmetic / relational predicates over input bytes; only a satisfying assignment returns success
Technique class (concepts only). Encoding decompiled predicates as SMT constraints and asking a solver for a model — teaching RE, not a remote exploit.
Impact. Contest flag recovery only.
Lessons.
- When human-solving a constraint thicket is painful, translating checks into an SMT solver is a standard lab skill
- Keep production validators simple and well-tested; “pretzel” predicates are fine for CTFs, poor for maintainable auth
Solve steps and PoC omitted.