# 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}`