Summary

• Serial format: XXXXXXXX-XXXXXXXX-XXXXXXXX-XXXXXXXX (32 hex digits, 3 dashes).
• Validation: Name and serial are combined via FNV-1a hashing and a splitmix64-style mix; a single final comparison decides success.
• Elegant weakness: One conditional jump controls the outcome. Patching that jump makes the program accept any valid-format input.

Challenge archive: Download froggy_crackme.zip

Solver script: froggy_solver.py (view or download the keygen source)

1. Validation flow (from reversing)

1. Anti-debug: reads /proc/self/status and checks TracerPid:. If non-zero - "Debugger detected. The swamp rejects you."
2. Input: prompts for Name and Serial (format above).
3. Serial parsing: 4 groups of 8 hex digits into two 64-bit values: v17 = (group1 << 32) | group2 and v18 = (group3 << 32) | group4.
4. Name hashes (FNV-1a, prime 0x100000001B3): v29 = hash(name) ^ 0xA3B1957C4D2E1901, v47 = hash(reverse(name)) ^ 0xC0D0E0F112233445.
5. Empty name fallback: v29 = 0xB7D49ACC3EB31A82, v47 = 0xD4B5EF4161BE37C6.
6. Final check: splitmix64-style chain combines v29, v47, v17, v18 and compares to 0xB9229933597558C9.

Target constant: 0xB9229933597558C9
Comparison: cmp rcx, rax at 0x2731
Conditional jump (failure path): 0x2734

2. Single path / elegant weakness

Success is decided by one comparison and one conditional jump:

• 0x2731: cmp rcx, rax (computed value vs 0xB9229933597558C9)
• 0x2734: conditional jump (e.g. jnz to "Wrong incantation" at 0x27ac)

If the jump is never taken, execution always reaches "The Swamp Gate opens."

Patch (elegant crack)

• File: froggy_crackme (or your copy).
• Location: the 2-byte instruction immediately after cmp rcx, rax (conditional jump at 0x2734).
• Original: conditional jump (e.g. 75 xx = jnz).
• Patch: replace those 2 bytes with 90 90 (NOP NOP).

Then run without a debugger (or with TracerPid cleared) and test any valid format:

Name: Froggy
Serial: 00000000-00000000-00000000-00000000

The program will always open the gate.

3. Finding a valid key (no patch) - Z3 keygen

To get a real name+serial pair that passes without patching, model the check in Z3 and solve for the four 32-bit serial parts.

The solver froggy_solver.py does the following:

1. From the name: compute FNV-1a hashes for name and reversed name, then apply known XORs to get v29 and v47.
2. fmix-like: reconstruct the binary mix (without final ^ (x >> 32) where applicable). Final comparison uses final_mix(x) = fmix_like(x) ^ (fmix_like(x) >> 32).
3. Serial as unknowns: four 32-bit values p0, p1, p2, p3 with v17 = (p0 << 32) | p1, v18 = (p2 << 32) | p3.
4. Formula: build v54, v55, v56, v57, v58 from decompiled logic and add final_mix(v58) == TARGET.
5. Z3: use bit-vector solver (QF_BV) with multiple seeds/timeouts to find satisfying values and format serial as XXXXXXXX-XXXXXXXX-XXXXXXXX-XXXXXXXX.

Usage

python3 froggy_solver.py
# dependency:
pip install z3-solver

Enter a name when prompted (e.g. Froggy). The solver tries a 15s timeout first, then 60s if needed.

Relevant code (excerpt)

• fnv1a64(data) - FNV-1a 64-bit hash.
• fmix_like(x) - mix used for v52, v53, v57 (without final xor with >>32).
• final_mix(x) - compared to TARGET: fmix_like(x) ^ (fmix_like(x) >> 32).
• solve_for_name(name, per_seed_timeout_ms) - builds the model and returns serial or (None, None).

4. Quick reference