HIP7CTF_Writeups/de/gatekeeper.md

The Gatekeeper

gatekeeper ist eine Reverse-Engineering-Challenge, die eine software-simulierte Hardwareschaltung beinhaltet. Uns wird eine Binärdatei bereitgestellt und wir müssen die Eingabe finden, die den Stromkreis "vervollständigt" und die LED einschaltet.

Informationsbeschaffung

Zuerst analysieren wir die Binärdatei:

$ file gatekeeper
gatekeeper: ELF 64-bit LSB pie executable, x86-64, ... stripped

Es ist eine gestrippte, statisch gelinkte 64-Bit-ELF-ausführbare Datei. Wenn sie ausgeführt wird, fragt sie nach einer Flagge.

$ ./gatekeeper
--- THE GATEKEEPER ---
Enter the flag that lights up the LED: AAAA
LED is OFF

Reverse Engineering

1. Analyse von Main (FUN_00108860)

Wir öffnen die Binärdatei in Ghidra und lokalisieren die main-Funktion bei 0x00108860.

undefined8 main(void)
{
  // ... Stack-Setup ...
  
  FUN_00114970("--- THE GATEKEEPER ---");
  do {
    FUN_00153610(1, "Enter the flag that lights up the LED: ");
    
    // Benutzereingabe lesen
    lVar1 = FUN_00114410(local_1e8, 0x80, PTR_DAT_001d4d78);
    if (lVar1 == 0) break;
    
    // Längenprüfung
    lVar1 = thunk_FUN_001246c0(local_1e8);
    if (lVar1 == 36) { 
      
      // ... (Komplexe Logik zur Erweiterung von 36 Zeichen in 288 Bits) ...
      
      // Löschen eines großen Arrays bei 0x1d6940 (Cache/Memoization)
      puVar6 = &DAT_001d6940;
      for (lVar1 = 0x1ba; lVar1 != 0; lVar1 = lVar1 + -1) {
        *puVar6 = 0;
        puVar6 = puVar6 + 1;
      }

      // Aufruf der Verifizierungsfunktion
      // Sie nimmt 0x374 (884) als erstes Argument und das Bit-Array als zweites
      iVar2 = FUN_001090d0(0x374, &local_168);
      
      if (iVar2 == 1) {
        FUN_00114970("LED is ON");
        return 0;
      }
    }
    FUN_00114970("LED is OFF");
  } while( true );
}

Aus main lernen wir:

1. Die Flagge muss genau 36 Zeichen lang sein.
2. Die Eingabe wird in ein Array von Bits umgewandelt.
3. Eine Verifizierungsfunktion FUN_001090d0 wird aufgerufen, beginnend mit dem Index 884.

2. Identifizierung der Gatterlogik (FUN_001090d0)

Die Funktion FUN_001090d0 bestimmt, ob unsere Eingabe korrekt ist. Sie fungiert als rekursiver Auswerter für eine Logikschaltung.

Sie akzeptiert einen gate_index als Argument. Sie verwendet diesen Index, um eine Gatterstruktur aus einem globalen Array bei 0x001d1020 nachzuschlagen. Jede Gatterstruktur enthält einen Opcode und Indizes für andere Gatter (Eingänge).

Der rekursive Prozess: Wenn die Funktion ein Gatter auswertet (z.B. ein UND-Gatter), kann sie das Ergebnis nicht sofort wissen. Stattdessen muss sie zuerst den Zustand der Eingänge bestimmen, die in dieses Gatter einspeisen.

1. Sie ruft sich selbst (FUN_001090d0) mit dem Index des linken Kindes auf.
2. Sie ruft sich selbst mit dem Index des rechten Kindes auf.
3. Sie führt die Logikoperation (UND/ODER/XOR) auf diesen beiden Ergebnissen aus und gibt den Wert zurück.

Diese Rekursion setzt sich tief in den Schaltungsbaum fort, bis sie auf einen "Basisfall" trifft: ein INPUT-Gatter (Fall 0). Das INPUT-Gatter liest einfach ein Bit aus unserer Flagge und gibt es zurück, wodurch die Rekursion für diesen Zweig gestoppt wird. Die Werte wandern dann den Baum wieder hinauf zur Wurzel.

Durch die Analyse der switch-Anweisung im Inneren können wir die spezifischen Operationen identifizieren:

Fall 1: UND-Gatter

Diese Logik repräsentiert eine UND-Operation. Beachten Sie die Rekursion: Es wertet zuerst das linke Kind aus. Wenn das 0 zurückgibt, wird kurzgeschlossen und 0 zurückgegeben. Andernfalls wird das rechte Kind ausgewertet.

case 1:
  // Rekursiver Aufruf für linkes Kind
  if (FUN_001090d0(left_idx) == 0) {
    result = 0;
  } else {
    // Rekursiver Aufruf für rechtes Kind
    result = FUN_001090d0(right_idx);
  }
  return result;

Fall 2: ODER-Gatter

Ähnlich wie UND, gibt aber 1 zurück, wenn das linke Kind 1 ist.

case 2:
  if (FUN_001090d0(left_idx) == 1) {
    result = 1;
  } else {
    result = FUN_001090d0(right_idx);
  }
  return result;

Fall 3: XOR-Gatter

Dies verwendet explizit den XOR-Operator auf den Ergebnissen der beiden rekursiven Aufrufe.

case 3:
  result = FUN_001090d0(left_idx) ^ FUN_001090d0(right_idx);
  return result;

Fall 4: NICHT-Gatter

Dieses Gatter hat nur einen Eingang (linkes Kind). Es ruft die Funktion rekursiv auf und invertiert das Ergebnis.

case 4:
  result = !FUN_001090d0(left_idx);
  return result;

Fall 0: INPUT-Gatter

Dies ist der Basisfall der Rekursion. Es ruft ein rohes Bit aus dem Eingabe-Array des Benutzers ab.

case 0:
  return input_bits[gate->bit_index];

Schlussfolgerung: Die Binärdatei ist ein Logikgatter-Simulator. Der Verifizierungsmechanismus ist eine große Schaltung (885 Gatter), die im .data-Abschnitt gespeichert ist. Wir müssen die Eingabebits finden, die dazu führen, dass das finale "Wurzel"-Gatter (884) eine logische 1 ausgibt.

Lösung

Wir können dies lösen, indem wir das Gatter-Array extrahieren und den Z3 Theorem Prover verwenden. Z3 ermöglicht es uns, die gesamte Schaltung als eine Menge von Bedingungen zu modellieren und die Eingabe zu finden, die diese erfüllt.

Solver-Skript

1. Gatter extrahieren: Jedes Gatter bei 0x1d1020 besteht aus 4 Integern: [Opcode, Left_Index, Right_Index, Bit_Index].
2. Variablen definieren: Erstelle 288 boolesche Variablen für die Flaggenbits.
3. Logik modellieren: Definiere rekursiv die Ausgabe jedes Gatters in Bezug auf Z3-Operatoren (z3.And, z3.Or, z3.Xor, z3.Not).
4. Lösen: Sage Z3, dass Gatter 884 Wahr sein muss.

import struct
import z3

FILENAME = "gatekeeper"
OFFSET = 0xd0020  # Datei-Offset für globales Array bei 0x1d1020
GATE_COUNT = 885
FLAG_LEN = 36

# In Ghidra identifizierte Opcodes
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. Schaltung aus Binärdatei laden
    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. Solver einrichten
    s = z3.Solver()
    input_bits = [z3.Bool(f'bit_{i}') for i in range(FLAG_LEN * 8)]
    gate_vars = {}

    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

    # 3. Behaupten, dass Wurzelgatter 1 ist
    s.add(get_var(GATE_COUNT - 1) == True)

    # 4. Ergebnis extrahieren
    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()

Ergebnis

Das Ausführen des Skripts liefert die Flagge: {flag: S0ftW4r3_d3F1n3d_l0g1c_G4t3s}