298 lines
9.4 KiB
Markdown
298 lines
9.4 KiB
Markdown
# The Gatekeeper
|
|
|
|
`gatekeeper` is a reverse engineering challenge involving a software-simulated hardware circuit. We are provided with a binary and must find the input that "completes the circuit" and turns the LED on.
|
|
|
|
## Information Gathering
|
|
|
|
We start by analyzing the binary:
|
|
|
|
```bash
|
|
$ file gatekeeper
|
|
gatekeeper: ELF 64-bit LSB pie executable, x86-64, ... stripped
|
|
```
|
|
|
|
It is a stripped, statically linked 64-bit ELF executable.
|
|
|
|
## Reverse Engineering
|
|
|
|
### 1. Analyzing Main (`FUN_00108860`)
|
|
|
|
We open the binary in Ghidra and locate the `main` function at `0x00108860`.
|
|
|
|
```c
|
|
undefined8 main(void)
|
|
{
|
|
// ... stack setup ...
|
|
|
|
FUN_00114970("--- THE GATEKEEPER ---");
|
|
do {
|
|
FUN_00153610(1, "Enter the flag that lights up the LED: ");
|
|
|
|
// Read user input
|
|
lVar1 = FUN_00114410(local_1e8, 0x80, PTR_DAT_001d4d78);
|
|
if (lVar1 == 0) break;
|
|
|
|
// Length Check
|
|
lVar1 = thunk_FUN_001246c0(local_1e8);
|
|
if (lVar1 == 36) {
|
|
|
|
// ... (Complex logic expanding 36 characters into 288 bits) ...
|
|
|
|
// Clear a large array at 0x1d6940 (Cache/Memoization)
|
|
puVar6 = &DAT_001d6940;
|
|
for (lVar1 = 0x1ba; lVar1 != 0; lVar1 = lVar1 + -1) {
|
|
*puVar6 = 0;
|
|
puVar6 = puVar6 + 1;
|
|
}
|
|
|
|
// Call the Verification Function
|
|
// It takes 0x374 (884) as the first argument and the bit array as the second
|
|
iVar2 = FUN_001090d0(0x374, &local_168);
|
|
|
|
if (iVar2 == 1) {
|
|
FUN_00114970("LED is ON");
|
|
return 0;
|
|
}
|
|
}
|
|
FUN_00114970("LED is OFF");
|
|
} while( true );
|
|
}
|
|
```
|
|
|
|
From `main`, we learn:
|
|
1. The flag must be exactly **36 characters** long.
|
|
2. The input is converted into an array of bits.
|
|
3. A verification function `FUN_001090d0` is called starting with index **884**.
|
|
|
|
### 2. Identifying the Gate Logic (`FUN_001090d0`)
|
|
|
|
The function `FUN_001090d0` determines if our input is correct. It acts as a recursive evaluator for a logic circuit.
|
|
|
|
It accepts a `gate_index` as an argument. It uses this index to look up a gate structure from a global array at `0x001d1020`. Each gate structure contains an opcode and indices for other gates (inputs).
|
|
|
|
**The Recursive Process:**
|
|
When the function evaluates a gate (e.g., an AND gate), it cannot know the result immediately. Instead, it must first determine the state of the inputs feeding into that gate.
|
|
1. It calls itself (`FUN_001090d0`) with the index of the **Left Child**.
|
|
2. It calls itself with the index of the **Right Child**.
|
|
3. It performs the logic operation (AND/OR/XOR) on those two results and returns the value.
|
|
|
|
This recursion continues deep into the circuit tree until it hits a "base case": an **INPUT** gate (Case 0). The INPUT gate simply reads a bit from our flag and returns it, stopping the recursion for that branch. The values then bubble back up the tree to the root.
|
|
|
|
By analyzing the `switch` statement inside, we can identify the specific operations:
|
|
|
|
#### Case 1: AND Gate
|
|
This logic represents an AND operation. Note the recursion: it evaluates the left child first. If that returns 0, it short-circuits and returns 0. Otherwise, it evaluates the right child.
|
|
```c
|
|
case 1:
|
|
// Recursive call for Left Child
|
|
if (FUN_001090d0(left_idx) == 0) {
|
|
result = 0;
|
|
} else {
|
|
// Recursive call for Right Child
|
|
result = FUN_001090d0(right_idx);
|
|
}
|
|
return result;
|
|
```
|
|
|
|
#### Case 2: OR Gate
|
|
Similar to AND, but returns 1 if the left child is 1.
|
|
```c
|
|
case 2:
|
|
if (FUN_001090d0(left_idx) == 1) {
|
|
result = 1;
|
|
} else {
|
|
result = FUN_001090d0(right_idx);
|
|
}
|
|
return result;
|
|
```
|
|
|
|
#### Case 3: XOR Gate
|
|
This explicitly uses the XOR operator on the results of the two recursive calls.
|
|
```c
|
|
case 3:
|
|
result = FUN_001090d0(left_idx) ^ FUN_001090d0(right_idx);
|
|
return result;
|
|
```
|
|
|
|
#### Case 4: NOT Gate
|
|
This gate only has one input (Left Child). It calls the function recursively and inverts the result.
|
|
```c
|
|
case 4:
|
|
result = !FUN_001090d0(left_idx);
|
|
return result;
|
|
```
|
|
|
|
#### Case 0: INPUT Gate
|
|
This is the base case of the recursion. It retrieves a raw bit from the user's input array.
|
|
```c
|
|
case 0:
|
|
return input_bits[gate->bit_index];
|
|
```
|
|
|
|
**Conclusion:**
|
|
The binary is a **logic gate simulator**. The verification mechanism is a large circuit (885 gates) stored in the `.data` section. We need to find the input bits that cause the final "root" gate (884) to output a logic `1`.
|
|
|
|
## Solution
|
|
|
|
We can solve this by using the **Z3 Theorem Prover**. Z3 is essentially an "inverse calculator." We can explain the rules of the circuit to Z3 (e.g., "Gate 5 is the XOR of Gate 3 and Gate 4") and then ask it "What input bits make the final gate equal 1?". Z3 will mathematically find the correct combination of bits.
|
|
|
|
We will build the solution script step-by-step.
|
|
|
|
### 1. Extracting the Circuit
|
|
First, we need to read the raw data of the 885 gates from the binary. Each gate is 16 bytes: `[Opcode, Left_ID, Right_ID, Value]`. We read this data into a Python dictionary.
|
|
|
|
```python
|
|
import struct
|
|
import z3
|
|
|
|
FILENAME = "gatekeeper"
|
|
OFFSET = 0xd0020 # Location of the gate array in the file
|
|
GATE_COUNT = 885
|
|
|
|
# Define opcodes for readability
|
|
OP_INPUT, OP_AND, OP_OR, OP_XOR, OP_NOT = range(5)
|
|
|
|
class Gate:
|
|
def __init__(self, op, left, right, val):
|
|
self.op, self.left, self.right, self.val = op, left, right, val
|
|
|
|
# Load the circuit structure
|
|
gates = {}
|
|
with open(FILENAME, "rb") as f:
|
|
f.seek(OFFSET)
|
|
for i in range(GATE_COUNT):
|
|
data = f.read(16)
|
|
# Unpack 4 integers (little-endian)
|
|
op, left, right, val = struct.unpack("<iiii", data)
|
|
gates[i] = Gate(op, left, right, val)
|
|
```
|
|
|
|
### 2. Defining Z3 Variables
|
|
We create 288 variables to represent the bits of our flag (36 characters * 8 bits). These are the "unknowns" Z3 needs to solve for.
|
|
|
|
```python
|
|
s = z3.Solver()
|
|
# Create 288 boolean variables: bit_0, bit_1, ... bit_287
|
|
input_bits = [z3.Bool(f'bit_{i}') for i in range(36 * 8)]
|
|
```
|
|
|
|
### 3. Modeling the Logic
|
|
We need a function that translates our Gate objects into Z3 logical expressions. This function is recursive, mirroring the structure of `FUN_001090d0`.
|
|
- If we encounter an **AND** gate, we tell Z3: "The value of this gate is `And(value_of_left, value_of_right)`".
|
|
- If we encounter an **INPUT** gate, we tell Z3: "The value of this gate is `input_bits[value]`".
|
|
|
|
We use a cache (`gate_vars`) to ensure we don't process the same gate multiple times, which keeps the script efficient.
|
|
|
|
```python
|
|
gate_vars = {}
|
|
|
|
def get_var(idx):
|
|
if idx in gate_vars: return gate_vars[idx]
|
|
|
|
g = gates[idx]
|
|
|
|
if g.op == OP_INPUT:
|
|
# Link this gate directly to one of our unknown flag bits
|
|
res = input_bits[g.val]
|
|
elif g.op == OP_AND:
|
|
res = z3.And(get_var(g.left), get_var(g.right))
|
|
elif g.op == OP_OR:
|
|
res = z3.Or(get_var(g.left), get_var(g.right))
|
|
elif g.op == OP_XOR:
|
|
res = z3.Xor(get_var(g.left), get_var(g.right))
|
|
elif g.op == OP_NOT:
|
|
res = z3.Not(get_var(g.left))
|
|
|
|
gate_vars[idx] = res
|
|
return res
|
|
```
|
|
|
|
### 4. Solving and Reconstructing
|
|
Finally, we add the constraint that the **Root Gate (884)** must be True. Then we ask Z3 to solve. If successful, we convert the resulting bits back into ASCII characters.
|
|
|
|
```python
|
|
# The final gate must output 1 (True)
|
|
s.add(get_var(GATE_COUNT - 1) == True)
|
|
|
|
if s.check() == z3.sat:
|
|
m = s.model()
|
|
# Convert the boolean model back to 0s and 1s
|
|
bits = [1 if m.evaluate(input_bits[i]) else 0 for i in range(36 * 8)]
|
|
|
|
flag = ""
|
|
for i in range(36):
|
|
char_val = 0
|
|
for b in range(8):
|
|
# Reconstruct the byte from 8 bits
|
|
if bits[i*8 + (7-b)] == 1: char_val |= (1 << b)
|
|
flag += chr(char_val)
|
|
print(f"Flag: {flag}")
|
|
```
|
|
|
|
### Complete Solver Script
|
|
|
|
```python
|
|
import struct
|
|
import z3
|
|
|
|
FILENAME = "gatekeeper"
|
|
OFFSET = 0xd0020
|
|
GATE_COUNT = 885
|
|
FLAG_LEN = 36
|
|
|
|
OP_INPUT, OP_AND, OP_OR, OP_XOR, OP_NOT = range(5)
|
|
|
|
class Gate:
|
|
def __init__(self, op, left, right, val):
|
|
self.op, self.left, self.right, self.val = op, left, right, val
|
|
|
|
def solve():
|
|
# 1. Load circuit
|
|
gates = {}
|
|
with open(FILENAME, "rb") as f:
|
|
f.seek(OFFSET)
|
|
for i in range(GATE_COUNT):
|
|
data = f.read(16)
|
|
op, left, right, val = struct.unpack("<iiii", data)
|
|
gates[i] = Gate(op, left, right, val)
|
|
|
|
# 2. Setup Solver
|
|
s = z3.Solver()
|
|
input_bits = [z3.Bool(f'bit_{i}') for i in range(FLAG_LEN * 8)]
|
|
gate_vars = {}
|
|
|
|
# 3. Recursive Logic Model
|
|
def get_var(idx):
|
|
if idx in gate_vars: return gate_vars[idx]
|
|
g = gates[idx]
|
|
|
|
if g.op == OP_INPUT: res = input_bits[g.val]
|
|
elif g.op == OP_AND: res = z3.And(get_var(g.left), get_var(g.right))
|
|
elif g.op == OP_OR: res = z3.Or(get_var(g.left), get_var(g.right))
|
|
elif g.op == OP_XOR: res = z3.Xor(get_var(g.left), get_var(g.right))
|
|
elif g.op == OP_NOT: res = z3.Not(get_var(g.left))
|
|
|
|
gate_vars[idx] = res
|
|
return res
|
|
|
|
# 4. Assert Root Gate is True
|
|
s.add(get_var(GATE_COUNT - 1) == True)
|
|
|
|
# 5. Extract Result
|
|
if s.check() == z3.sat:
|
|
m = s.model()
|
|
bits = [1 if m.evaluate(input_bits[i]) else 0 for i in range(FLAG_LEN * 8)]
|
|
flag = ""
|
|
for i in range(FLAG_LEN):
|
|
char_val = 0
|
|
for b in range(8):
|
|
if bits[i*8 + (7-b)] == 1: char_val |= (1 << b)
|
|
flag += chr(char_val)
|
|
print(f"Flag: {flag}")
|
|
|
|
solve()
|
|
```
|
|
|
|
### Result
|
|
Running the script yields the flag:
|
|
`{flag: S0ftW4r3_d3F1n3d_l0g1c_G4t3s}` |