8.8 KiB
The Clockwork
the_clockwork is a reverse engineering challenge involving a system of interdependent equations. We are provided with a binary challenge and need to find the correct input to satisfy its internal logic.
Information Gathering
$ file challenge
challenge: ELF 64-bit LSB executable, x86-64, ... not stripped
The binary is not stripped, revealing function names. We analyze it using Ghidra.
Reverse Engineering
Main Function
We locate the main function (0x402057). The decompilation reveals the initialization of a target array and a loop verifying the calculated "gears".
undefined8 main(void)
{
bool bVar1;
int iVar2;
char *pcVar3;
size_t sVar4;
long in_FS_OFFSET;
int local_164;
int local_158 [64];
char local_58 [72];
long local_10;
local_10 = *(long *)(in_FS_OFFSET + 0x28);
local_158[0] = 0x174;
local_158[1] = 0x2fe;
local_158[2] = 0x3dc;
local_158[3] = 0x30c;
local_158[4] = 0xfffffe57;
local_158[5] = 0xffffffc6;
local_158[6] = 0x28a;
local_158[7] = 0x23d;
local_158[8] = 0x24d;
local_158[9] = 0xee;
local_158[10] = 0x183;
local_158[0xb] = 0x124;
local_158[0xc] = 0x1e0;
local_158[0xd] = 0x19c;
local_158[0xe] = 0x1ab;
local_158[0xf] = 0x444;
// ... (initialization continues for 32 values) ...
local_158[0x1f] = 0x209;
// ... (input reading logic) ...
if (sVar4 == 0x20) {
// Calculate gears, storing result in the second half of local_158
calculate_gears(local_58,local_158 + 0x20);
bVar1 = true;
local_164 = 0;
goto LAB_00402348;
}
// ...
LAB_00402348:
if (0x1f < local_164) goto LAB_00402351;
// Constraint Check:
// gears[next] * 2 + gears[current] == target[current]
// where next = (current + 1) % 32
if (local_158[(long)((local_164 + 1) % 0x20) + 0x20] * 2 + local_158[(long)local_164 + 0x20] !=
local_158[local_164]) {
bVar1 = false;
goto LAB_00402351;
}
local_164 = local_164 + 1;
goto LAB_00402348;
// ...
}
The loop at LAB_00402348 verifies that for every gear i:
gears[i] + 2 * gears[(i+1)%32] == target[i]
Calculate Gears
The function calculate_gears computes the gears array from the input string.
void calculate_gears(char *param_1,undefined4 *param_2)
{
undefined4 uVar1;
uVar1 = f0((int)*param_1);
*param_2 = uVar1;
uVar1 = f1((int)param_1[1],*param_2);
param_2[1] = uVar1;
uVar1 = f2((int)param_1[2]);
param_2[2] = uVar1;
uVar1 = f3((int)param_1[3],param_2[2]);
param_2[3] = uVar1;
// ... Pattern continues ...
uVar1 = f30((int)param_1[0x1e]);
param_2[0x1e] = uVar1;
uVar1 = f31((int)param_1[0x1f],param_2[0x1e]);
param_2[0x1f] = uVar1;
return;
}
It uses 32 helper functions (f0 through f31).
- Even indices depend only on the input character:
gears[i] = f_i(input[i]) - Odd indices depend on the input and the previous gear:
gears[i] = f_i(input[i], gears[i-1])
Solution
Solving this challenge manually would be difficult because the equations are cyclic: gears[0] affects gears[1], which affects gears[2]... and the verification loop wraps around so that gears[31] affects gears[0].
Instead of calculating it by hand, we can use Z3, a powerful theorem prover from Microsoft. Z3 allows us to describe the problem as a set of logic constraints (e.g., "x is an integer," "y = x + 5," "y must equal 10") and then asks the engine to find values for x and y that satisfy all statements.
Solver Construction
We build the solver step-by-step.
1. Define Inputs We start by defining our unknown inputs. We know the flag is 32 characters long, so we create 32 32-bit BitVectors. We also constrain them to be printable ASCII (32-126) because we know the flag is a string.
2. Define Targets
We extract the target values directly from the main function's stack initialization code. These are the values our gears must align with.
3. Replicate Helper Functions
We need to tell Z3 how to calculate the gears. We take the logic from f0, f1, etc., and rewrite it in Python.
For example, f0 in C is return (char)(param_1 ^ 0x55) + 10;.
In Python for Z3, we write return c_char(p1 ^ 0x55) + 10.
Note that f1 uses modulo 200. In C, % on negative numbers can be tricky, but SRem (Signed Remainder) in Z3 matches the C behavior.
4. Build the Gears Array
We programmatically construct the list of gear values.
gears[0] is the result of f0(flag[0]).
gears[1] is the result of f1(flag[1], gears[0]).
We do this for all 32 gears, following the pattern found in calculate_gears.
5. Add Constraints
Finally, we add the condition found in the main loop: gears[i] + 2 * gears[(i+1)%32] == targets[i]. This links everything together into a solvable system.
6. Solve
We ask Z3 to check if there is a solution (s.check()). If it finds one, we extract the values of our flag variables and print them as characters.
Final Solver Script
import z3
s = z3.Solver()
# 1. Define inputs (32 chars)
flag = [z3.BitVec(f'flag_{i}', 32) for i in range(32)]
# 2. Constrain to Printable ASCII (The only hint we need)
for i in range(32):
s.add(flag[i] >= 32)
s.add(flag[i] <= 126)
# 3. The Target Values (Extracted from your decompilation)
# These correspond to local_158[0] through local_158[31]
targets = [
0x174, 0x2fe, 0x3dc, 0x30c, 0xfffffe57, 0xffffffc6, 0x28a, 0x23d,
0x24d, 0xee, 0x183, 0x124, 0x1e0, 0x19c, 0x1ab, 0x444,
0xffffffc8, 0xffffff4c, 0x13c, 0x25e, 0x1fe, 0x18a, 200, 0x82,
0x233, 0x2da, 0x36e, 0x3c3, 0x47d, 0x2a4, 0x3b5, 0x209
]
# ---------------------------------------------------------
# HELPER FUNCTIONS (The Gears)
# We use the Unsigned Logic (0-255) that worked for you before.
# ---------------------------------------------------------
def c_char(x): return x & 0xFF # Treat char as unsigned (0-255)
def c_rem(a, b): return z3.SRem(a, b) # Signed Remainder
def f0(p1): return c_char(p1 ^ 0x55) + 10
def f1(p1, p2): return c_rem((p1 + p2), 200)
def f2(p1): return p1 * 3 - 20
def f3(p1, p2): return (p1 ^ p2) + 5
def f4(p1): return (p1 + 10) ^ 0xaa
def f5(p1, p2): return (p1 - p2) * 2
def f6(p1): return p1 + 100
def f7(p1, p2): return (p1 ^ p2) + 12
def f8(p1): return (p1 * 2) ^ 0xff
def f9(p1, p2): return p2 + p1 - 50
def f10(p1): return c_char(p1 ^ 123)
def f11(p1, p2): return c_rem((p1 * p2), 500)
def f12(p1): return p1 + 1
def f13(p1, p2): return (p1 ^ p2) * 2
def f14(p1): return p1 - 10
def f15(p1, p2): return (p2 + p1) ^ 0x33
def f16(p1): return p1 * 4
def f17(p1, p2): return (p1 - p2) + 100
def f18(p1): return c_char(p1 ^ 0x77)
def f19(p1, p2): return c_rem((p1 + p2), 150)
def f20(p1): return p1 * 2
def f21(p1, p2): return (p1 ^ p2) - 20
def f22(p1): return p1 + 33
def f23(p1, p2): return (p2 + p1) ^ 0xcc
def f24(p1): return p1 - 5
def f25(p1, p2): return c_rem((p1 * p2), 300)
def f26(p1): return p1 ^ 0x88
def f27(p1, p2): return p2 + p1 - 10
def f28(p1): return p1 * 3
def f29(p1, p2): return (p1 ^ p2) + 44
def f30(p1): return p1 + 10
def f31(p1, p2): return (p2 + p1) ^ 0x99
# ---------------------------------------------------------
# CALCULATE GEARS
# ---------------------------------------------------------
gears = [0] * 32
gears[0] = f0(flag[0])
gears[1] = f1(flag[1], gears[0])
gears[2] = f2(flag[2])
gears[3] = f3(flag[3], gears[2])
gears[4] = f4(flag[4])
gears[5] = f5(flag[5], gears[4])
gears[6] = f6(flag[6])
gears[7] = f7(flag[7], gears[6])
gears[8] = f8(flag[8])
gears[9] = f9(flag[9], gears[8])
gears[10] = f10(flag[10])
gears[11] = f11(flag[11], gears[10])
gears[12] = f12(flag[12])
gears[13] = f13(flag[13], gears[12])
gears[14] = f14(flag[14])
gears[15] = f15(flag[15], gears[14])
gears[16] = f16(flag[16])
gears[17] = f17(flag[17], gears[16])
gears[18] = f18(flag[18])
gears[19] = f19(flag[19], gears[18])
gears[20] = f20(flag[20])
gears[21] = f21(flag[21], gears[20])
gears[22] = f22(flag[22])
gears[23] = f23(flag[23], gears[22])
gears[24] = f24(flag[24])
gears[25] = f25(flag[25], gears[24])
gears[26] = f26(flag[26])
gears[27] = f27(flag[27], gears[26])
gears[28] = f28(flag[28])
gears[29] = f29(flag[29], gears[28])
gears[30] = f30(flag[30])
gears[31] = f31(flag[31], gears[30])
# ---------------------------------------------------------
# ADD CONSTRAINTS (The Chain Link)
# Logic: gears[i] + 2 * gears[next] == target[i]
# ---------------------------------------------------------
for i in range(32):
next_idx = (i + 1) % 32
s.add((gears[i] + gears[next_idx] * 2) == targets[i])
# ---------------------------------------------------------
# SOLVE
# ---------------------------------------------------------
print("Solving new unique constraints...")
if s.check() == z3.sat:
m = s.model()
result = ""
for i in range(32):
result += chr(m[flag[i]].as_long())
print("\n[+] FOUND FLAG:", result)
else:
print("unsat - No solution found.")