re-z3

Z3 constraint solving (modeling / key and flag derivation)

When to use / when not to use

• Use: when a set of comparison chains / mathematical equations that "a valid input must satisfy" (e.g., serial = f(username), flag byte-by-byte satisfying some relation) has been recovered from decompilation, and manual back-derivation is tedious, hand it to the solver
• Use: CTF reversing challenges / key / flag derivation for crypto challenges (the verification logic is pure deterministic computation with no syscall dependency)
• Use: when there are already manually unrolled loop-body (bitwise XOR / shift / add-sub) constraints, and you want to verify whether the constraint set is complete (see Pitfall 4)
• Don't use: when the input is checked byte-by-byte inside a long loop and the loop is not unrolled—first use [[re-angr]] symbolic execution or unroll manually first (this skill requires constraints to be restored to expressions first, see Pitfall 2)
• Don't use: when the constraints involve irreversible operations such as hashing / asymmetric signature verification—Z3 is powerless against SHA / RSA signature verification (see Pitfall 3)
• Don't use: when you need the entire path condition rather than a set of constraints—[[re-angr]] is more suitable
• Note: modeling must be done line-by-line against the decompiled pseudocode ([[re-ghidra]] / [[re-ida]] / [[re-radare2]] output); run the solved result through the original program to verify (sandbox, [[re-analyze/platform-tips]] highest principle)

Tool preparation

Refer to [[re-analyze/platform-tips]] highest principle—solving itself does not execute the target, but when using the solving result to run the target for verification, default to a sandbox.

z3-solver (pip install)

• pip install z3-solver(prebuilt wheels available for Linux / macOS / Windows; pure Python bindings + native library, simple to install)
• If mixing with the system package manager causes conflicts (system z3 version is old): first pip install --upgrade z3-solver, or install inside a separate venv
• Verify: python3 -c "import z3; print(z3.get_version_string())"
• No network environment: offline wheel (pip download z3-solver then copy in) or system package apt install z3(note the API differences between the system z3 Python bindings and the pip version; pip version recommended)

python3

• Linux: apt install python3(mostly bundled); macOS: brew install python; Windows: official installer / choco install python
• Verify: python3 --version

Decompilation output (the raw material for constraint restoration)

• Decompiled pseudocode of the verification function from [[re-ghidra]] / [[re-ida]] / [[re-radare2]]—comparison chains, each arithmetic / XOR / shift / table-lookup transformation, and the final comparison method (strcmp / check digit / byte-by-byte comparison); export function-level pseudocode as the reference for line-by-line modeling (see Pitfall 4)
• Verify: the pseudocode fully covers every constraint that "a valid input must satisfy"

Operating steps

Execute in order, recording the result of each step (constraint list / modeling script / solver output / verification result, for evidence paths see [[re-triage]]).

1. Restore constraints from decompilation (comparison chains / mathematical relations)：

   • Listeveryconstraint that "a valid input must satisfy": input source (user input / filename / ciphertext), each transformation (arithmetic / XOR / shift / table lookup), final comparison method (if (a == b) / check digit equality / byte-by-byte strcmp)
   • Convert each one into a mathematical expression and write it as a list (pseudocode line → constraint expression, one-to-one correspondence, see Pitfall 4):
     • if (x * 3 + 5 != 0x100) fail → x*3 + 5 == 0x100
     • Loop already unrolled:for (i=0;i<8;i++) out[i]=in[i]^key[i]; if(strcmp(out, s)) fail → 8 constraints in[i]^key[i] == s[i]
   • Do not skip any line——Skipped lines are the omitted constraints (see Pitfall 4); when encountering an irreversible segment (hash), mark it first, see Pitfall 3

2. BitVec / Int modeling：

   • Bitwise operations dominant (XOR / shifts / bitwise AND) → use BitVec, bit width aligned with decompiled semantics (for 32-bit operations use BitVec('x', 32), byte-by-byte use 8-bit)
   • Pure mathematical relations (add/subtract/multiply, comparisons, no bitwise operations) → use Int faster (but overflow semantics differ from C, see Pitfall 5)
   • Model according to input structure: character-by-character processing → an 8-bit BitVec array or use a large BitVec slice:

     from z3 import *
     s = Solver()
     inp = [BitVec(f'inp_{i}', 8) for i in range(8)]      # 8 字节输入
     

   • Bit width mismatch immediately causes problems：BitVec(..., 8) and BitVec(..., 32) directly added together will report TypeError / no solution——unify the width, see Pitfall 5

3. solver.check / model：

   • After all constraints s.add(...) :r = s.check() —— sat / unsat / unknown
   • sat → m = s.model() get solution;unsat → the constraint set is contradictory (see Pitfall 4 / Pitfall 5);unknown → nonlinear / complex expressions (see Pitfall 3)
   • Extract byte by byte:''.join(chr(m[inp[i]].as_long()) for i in range(8))(to get BitVec values use as_long()）
   • Solving is not one-shot: first addboundary constraintsthen check (see Step 4), whenunsat use s.assertions() to troubleshoot by commenting out constraints one by one (see Pitfall 4)

4. Boundary (length / character set) constraints：

   • Add boundaries before solving(unbounded variables will slow down solving or even run wild, see Pitfall 1):

     for c in inp:
         s.add(c >= 0x20, c <= 0x7e)      # 可打印 ASCII（flag 场景）
     s.add(inp[0] == ord('f'))            # 已知格式头 flag{ 逐位固化
     

   • Length constraint: input length fixed value (inp[7] == ord('}')); check bits / separator format supplemented according to decompilation
   • Parts already known from the problem clues / format (flag{...})directly fixed as equations, greatly speeding up
   • After adding boundaries, first do a small-scale verification: comment out some constraints and run once to see the solving time and whether the solution is reasonable

5. Output flag / key：

   • Assemble the output: concatenate the byte array in order into a string / hexadecimal, write it into flag.txt(or the key binary), and also print repr to check (printability)
   • Handling multiple solutions:while s.check() == sat: 取解 → s.add(Or(逐位 != 当前解)) enumerate multiple solutions and compare with the problem's expected value (see Pitfall 4)
   • Verification: in the sandbox ([[re-sandbox]]) feed the solver output as-is to the target program (stdin / arguments / file); it must pass validation / print the flag; then cross-check against [[re-angr]] / manual recovery results

Cross-domain integration

• [[re-ctf]]: this skill is the constraint-solving path of step 3 in the re-ctf gateway workflow ("satisfying a set of equations equals flag / key")
• [[re-binary-core]]: decompilation workbench ([[re-ghidra]] / [[re-ida]] / [[re-radare2]])——the raw material for constraint recovery; [[re-triage]] preliminary reconnaissance confirms architecture and bit width (basis for bit width modeling)
• [[re-angr]]: sister skill——use angr symbolic execution for long-loop byte-by-byte validation; for already expanded / loop-free constraint sets, this skill is lighter and faster; when angr solves slowly, convert a subset of constraints to z3
• [[re-keygen]] / [[re-license]]: keygen scenarios——model and solve the equation set where serial number = f(username / machine code) (the re-keygen tool is preparing to list z3 as an optional solution; the re-cracking gateway uses it as a brute-force means outside irreversible algorithms)
• [[re-crypto-id]] / [[re-crypto-decrypt]]: key / plaintext derivation for custom encryption (model the reversible part of the equation; for the pure hash part see pitfall 3)
• [[re-sandbox]]: run-validation sandbox for solution results ([[re-analyze/platform-tips]] highest principle)
• [[re-patching]]: when the constraints are unsolvable (including irreversible segments), switch to patching to bypass verification

Common pitfalls and traps

• Unbounded variables → slow solving / runaway: Symptom——s.check() does not return for tens of minutes, or memory explodes; Cause——symbolic variables have no range constraints, so the solver traverses a huge space (especially multiplication/division / shift combinations); Countermeasure——add bounds before solving(step 4: length / charset / bit-width upper limits), directly fix known format bits (flag{ header); if still slow, tighten the bounds and verify segment by segment
• Bit-width mismatch → no solution / error: Symptom——unsat but manually the constraints are clearly satisfiable, or TypeError: unsupported operand; Cause——mixing BitVecs of different bit widths (adding 8-bit and 32-bit, inconsistent shift widths), C implicit integer promotion not modeled (char operations promote to int then truncate); Countermeasure——check the pseudocode line by line to confirm the operation width (a 32-bit multiplication result takes only the low 32 bits = add Extract(31,0)); first restorethe minimal complete semanticsthen relax (see pitfall 5)
• Poor nonlinear operation support → change approach: Symptom——check() returns unknown, or solving is extremely slow when multiplication / XOR combinations are involved; Cause——nonlinear polynomials (multiplication/division, combinations of some bitwise operations) are difficult for SMT solvers; Countermeasure——simplify manually where possible first (XOR symmetry, constant folding, use modular inverse pow(a,-1,m) to eliminate methods); if still unknown → switch to [[re-angr]] symbolic execution of the whole path, or brute-force bit by bit (split constraints into single-byte solving);give up modeling hash / signature-verification segments directly(irreversible), switch to [[re-patching]] / honest reporting
• Missing constraints → wrong solution: Symptom——the input that solves as "satisfying" is rejected when the program is run; Cause——some line of the decompiled pseudocode was not translated into a constraint (length check, charset whitelist, boundary if branches, extra check bits), or the solver gives only one solution while the challenge requires a specific solution; Countermeasure——check the constraint list line by line against the pseudocode (the one-to-one correspondence table in step 1), add the missed if / checks into s.add; when there are multiple solutions, enumerate all solutions and run target verification one by one (step 5);unsat during troubleshooting, comment out constraints one by one to locate the contradiction
• Overflow / signed semantics not modeled: Symptom——the solved result value does not match the program's actual computation (sometimes right, sometimes wrong); Cause——C 32-bit signed overflow (int multiplication wraparound), shift direction (>> arithmetic / logical), endianness (big-endian target) not aligned; Countermeasure——determine the target architecture and bit width ([[re-triage]]), for signed operations use BitVec(..., 32) + sign extension to simulate, or switch to Int plus range constraints to simulate wraparound (s.add(a == (b * c) % 2**32)); endianness according to the target (most CTF challenges are little-endian)
• Hard-modeling long loops and giving them to z3 (challenges that should use angr): Symptom — manually expanding a long loop of byte-by-byte checks into constraints, where the expansion is wrong and causes unsat, or after expansion the solving is extremely slow; Cause — loop invariant extraction / expansion method is wrong, and the expansion scale is large; Countermeasure — for long loops / deep comparison chains, first use [[re-angr]] symbolic execution (automatically handles loops and paths), and let z3 only take over "loop-free, pure equality sets" (comparison chains extracted directly from Ghidra decompilation); cross-validate the results from both paths
• PRNG state recovery problems may return an incorrect model: Symptom —check() returns sat and the model values are reasonable, but when substituted back into the original program (e.g. an xorshift128+ generator) the output does not match, or there is simply no solution; Cause — some bit-vector problems (PRNG internal state recovery) are known difficulties for SMT solvers (Z3 4.12.x has known failure cases in recovering the two 64-bit state words of xorshift128+ from two outputs); Countermeasure — results must be cross-validated: substitute the model back into the target program and replay ([[re-sandbox]]), enumerate multiple solutions, or compare against [[re-angr]]/brute force (when the key space is small); sat does not guarantee correctness
• Hardcoding "observed values" as constant assertions → false unsat: Symptom —unsat but manual checking shows the constraints are clearly satisfiable; Cause — directly asserting experimentally observed intermediate values as equalities (e.g. RNG(seed).next(26) == 57508594, whereas the computation actually yields 14325532), making the equality always false; Countermeasure — first do not add assertions for intermediate observed values, and only assert the input-output relation to let Z3 infer the unknowns; if intermediate values really must be fixed, first use m.eval() to verify whether the observed values themselves are consistent with the model