Logoflag1

Platform: spbctf | Category: Reversing | Type: Challenge | Difficulty: Easy | OS: Linux | Author: XESXOR | Date: 2026-07-01 | Status: Solved Techniques: cross_platform_binary_verification_via_docker, manual_equation_extraction_from_asm, static_disassembly_analysis, z3_smt_solving

Summary

Task: 64-bit ELF (rev-kids20.forkbomb.ru task1) reads a string via gets() and passes it to a C++ test(char*) function that checks length==8 then 8 nonlinear integer equations over the input bytes. Solution: extracted the 8 equations directly from x86-64 disassembly and modeled them as a Z3 constraint system over 8 printable-ASCII integer variables, solved instantly to recover the flag.

Logoflag1 — spbctf

Description

(Source: rev-kids20.forkbomb.ru, task1) "Just give a valid flag." Binary download: https://rev-kids20.forkbomb.ru/files/rev/re8/task1

English summary: A single ELF binary (task1) is given with no other artifacts. It reads a line of input and reports "Valid flag" or "Invalid flag". The goal is to find an input string that the binary accepts as valid — that string itself is the flag (no spbCTF{...} wrapper was present anywhere in the binary).

Analysis

• file task1 → 64-bit ELF, x86-64, dynamically linked, not stripped, BuildID present. Not stripped meant symbol names (including the C++ mangled test function) were directly visible in objdump -d.
• main reads user input into a stack buffer using gets() — a classic unbounded-read primitive that would normally suggest a stack buffer overflow / ret2win path. This was considered as a candidate attack family, but it turned out to be a red herring / unused primitive: there is no win() function, no interesting gadget target, and the challenge is entirely a keygen-style algorithmic check. gets() here is simply lazy/unsafe input handling, not the intended exploitation vector. (Useful negative-hypothesis note: presence of an unsafe input function does not always mean the solve path is memory corruption — always check whether a simpler "satisfy the validator" path exists first.)
• After reading input, main calls _Z4testPc (Itanium C++ mangled name, demangles to test(char*)) with the input pointer and branches on the boolean return value to print "Valid flag" / "Invalid flag".
• Disassembling test(char*):
  • First check: strlen(input) == 8. Any other length returns false immediately — this pins the flag length at exactly 8 characters.
  • The function then evaluates a sequential chain of 8 blocks. Each block:
    1. Loads several input bytes via movzx/movsx (sign-extending char to int),
    2. Computes a small nonlinear arithmetic expression (imul, add, sub) combining 2–4 of the bytes,
    3. Compares the result against a hardcoded 32-bit immediate with cmp,
    4. On mismatch, calls printf with some debug/intermediate value and returns false — this printed value is NOT itself a required condition, it's just diagnostic output on the failure path of that specific equation and can be ignored for solving.
    5. On match, falls through to the next block.
  • Only if all 8 comparisons succeed does execution reach mov eax, 1 at address 0x400ba3 (success/return true).
• Reading the immediates and byte indices directly off the disassembly yielded 8 nonlinear equations over s0..s7 (the 8 input bytes as signed ints): ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

E1: s0 + 2*s5*s7            == 0x194e   (6478)
E2: s1 + s2 + s0*s4         == 0x203b   (8251)
E3: s0*s2 + s3 - s5         == 0x14e4   (5348)
E4: s0*s3 + s2 + s6         == 0xf14    (3860)
E5: s1 - s2 - s0*s3         == -3747    (0xfffff15d as 32-bit signed)
E6: s0 + s3 + s5*s6         == 0x191e   (6430)
E7: s1 + s6 + s0*s2         == 0x1585   (5509)
E8: s2*s3*s4 + s0*s5 - s2   == 0x5caa2  (380066)

This is a small nonlinear Diophantine-style system — not solvable cleanly by hand due to the products of variables (E8 has a triple product), but trivial for an SMT solver once each byte is bounded to a sane range (printable ASCII). ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Solution

1. Downloaded the binary and ran file / objdump -d -M intel task1 to disassemble.
2. Located main → gets() → call to _Z4testPc, and disassembled test(char*) fully (saved to test_func.txt).
3. Manually walked each of the 8 comparison blocks, extracting which bytes participate, the arithmetic operation, and the target immediate, translating each into an algebraic equation as shown above.
4. Modeled the 8 equations in Z3 with each byte constrained to [32, 126] (printable ASCII range) to keep the search space small and force a human-readable solution.
5. Solved instantly with Z3 → byte values [76, 48, 71, 49, 107, 97, 65, 33] → ASCII string REDACTED.
6. Verified correctness: since the binary is a Linux x86-64 ELF and the analysis host is Apple Silicon macOS, ran it inside a Docker container (--platform linux/amd64 ubuntu:22.04) and piped the candidate string to stdin:

   docker run --rm -v <taskdir>:/w -w /w --platform linux/amd64 ubuntu:22.04 \
     bash -c "echo 'REDACTED' | ./task1"
   

   Output: Valid flag — confirming the recovered string satisfies all 8 constraints and the length check. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

 python read-only • copy allowed Copy
#!/usr/bin/env python3
from z3 import *

s = [Int(f's{i}') for i in range(8)]

solver = Solver()
for x in s:
    solver.add(x >= 32, x <= 126)

s0,s1,s2,s3,s4,s5,s6,s7 = s

solver.add(s0 + 2*s5*s7 == 0x194e)
solver.add(s1 + s2 + s0*s4 == 0x203b)
solver.add(s0*s2 + s3 - s5 == 0x14e4)
solver.add(s0*s3 + s2 + s6 == 0xf14)
solver.add(s1 - s2 - s0*s3 == -3747)
solver.add(s0 + s3 + s5*s6 == 0x191e)
solver.add(s1 + s6 + s0*s2 == 0x1585)
solver.add(s2*s3*s4 + s0*s5 - s2 == 0x5caa2)

if solver.check() == sat:
    m = solver.model()
    vals = [m[x].as_long() for x in s]
    print(vals)
    print(''.join(chr(v) for v in vals))
else:
    print("unsat")

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