276 lines
8.8 KiB
Markdown
276 lines
8.8 KiB
Markdown
# 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
|
|
|
|
```bash
|
|
$ 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".
|
|
|
|
```c
|
|
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.
|
|
|
|
```c
|
|
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
|
|
|
|
```python
|
|
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.")
|
|
```
|