Finde die Flagge in
eine CTF-Binärdatei.

Finden Sie den Prüfcode

Das Handout ist eine 15 KB große ausführbare Datei. Es fragt nach einer Flagge und druckt dann Correct! oder Incorrect!. Beginnen Sie mit einer einfachen Anfrage an Ihren Agenten.

Eine Beispiel-Eingabeaufforderung, bei der die heruntergeladene Herausforderung lokal verfügbar ist und eine Analyse des Maschinencode-Programmanbieters verbunden ist.

1. Folgen Sie der Eingabeaufforderung zu ihrer Funktion

   Vertreter → REA

   open_binary
   {"path": "ms_flag_checker"}
   
   search_strings
   {"pattern": "flag|correct|wrong|input",
    "mode": "regex", "case_sensitive": false}
   
   xrefs
   {"address": "0x102004"}
   
   resolve_containing_procedure
   {"address": "0x10126d"}

   REA → Agent * ausgewählte Ergebnisse

   0x102004  "What is the flag? "
   0x10201c  "Incorrect!"
   0x102027  "Correct!"
   
   Prompt referenced at: 0x10126d
   Containing function: 0x10124d

   Die Referenz gibt dem Agenten einen Ort zum Untersuchen, obwohl die ursprünglichen Funktionsnamen der ausführbaren Datei entfernt wurden.

2. Lesen Sie den Checker und seine beiden Helfer

   Vertreter → REA

   analyze_function
   {"procedure": "0x10124d"}
   
   analyze_function
   {"procedure": "0x101189"}
   
   analyze_function
   {"procedure": "0x101217"}

   REA → Agent * ausgewählte Anweisungen

   0x1012c1: CMP EDI, 0x24
   0x1012c6: LEA RBX, [0x1040e0]
   0x1012cd: LEA RBP, [0x104060]
   0x1012d4: LEA R13, [RBX + 0x270]
   0x1012e1: CALL 0x00101189
   0x1012ec: CALL 0x00101217
   0x1012f1: CMP dword ptr [RBP], EAX
   0x1012f4: JNZ 0x00101335
   0x1012f6: ADD RBX, 0x18

   Die erste Schleife kopiert 36 Zeichencodes. Die Prüfschleife dekodiert eine Maske, summiert die ausgewählten Codes und vergleicht das Ergebnis mit einer gespeicherten Nummer. Seiner 0x18-byte-Schritte über 0x270 bytes ergeben 26 Masken.

Dies sind ausgewählte Ergebnisse einer neuen REA-Analyse. Der lokale Zielpfad wird für die Anzeige gekürzt; Adressen beziehen sich auf das importierte Bild von REA.

Ein Häkchen zeigt einen Charakter

Der Checker ordnet die Eingabe in einem 6 × 6-Raster an. Eine Maske wählt aus, welche Zellen zu einer Summe beitragen. Seine kompakte Codierung verwendet negative Zahlen, um Zellen zu überspringen, und positive Zahlen, um sie auszuwählen.

Lesen Sie die Maske und ihr Ziel aus der Binärdatei

{"address": "0x1040e0", "length": 624}
{"address": "0x104060", "length": 144}

Mask at 0x104170:
eb 01 f2 00  →  -21, +1, -14, stop

Target at 0x104078:
37 00 00 00  →  55

Anweisung MOVSX liest Maskenbytes als vorzeichenbehaftete Werte. Das ist der Grund eb bedeutet -21. Das Ziel ist eine Little-Endian-Ganzzahl. Zusammen sagen diese Bytes dem Agenten, dass code[21] = 55, also ist dieser Charakter 7.

Von der Anleitung zum lesbaren Scheck

Wählen Sie einen Schritt aus, um den Summierungshelfer und seinen Aufrufer mit derselben Regel in C zu verbinden.

0x10121c: MOV ECX, 0x0

0x10122c: CMP dword ptr [RSI + RAX*0x1], 0x0
0x101230: JZ 0x00101223

0x101232: ADD ECX, dword ptr [RDI + RAX*0x1]

0x101223: ADD RAX, 0x4

0x1012f1: CMP dword ptr [RBP], EAX
0x1012f4: JNZ 0x00101335

int check_one_mask(const int codes[36],
                   const int mask[36],
                   int target) {
    int total = 0;
    for (int i = 0; i < 36; ++i) {
        if (mask[i]) {
            total += codes[i];
        }
    }
    return total == target;
}

Die Anweisungen stammen vom Summierhelfer und seinem Aufrufer. Das C ist eine erklärende Zusammenfassung mit beschreibenden Namen und einer abgeflachten 36-Zellen-Schleife.

Löse die 26 Gleichungen

Die meisten Masken markieren mehrere Zellen. Zum Beispiel fügt die erste Prüfung 16 Zeichencodes hinzu und erfordert insgesamt 1441. Die überlappenden Auswahlen ergeben Gleichungen, die ein kleines Python-Skript zusammen lösen kann.

from z3 import Int, Or, Solver, Sum, sat

codes = [Int(f"code_{i}") for i in range(36)]
solver = Solver()
alphabet = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_{}"
for code in codes:
    solver.add(Or(*[code == ord(c) for c in alphabet]))
for code, char in zip(codes, "DUCTF{"):
    solver.add(code == ord(char))
solver.add(codes[-1] == ord("}"))

for selected, target in checks:
    solver.add(Sum([codes[i] for i in selected]) == target)

assert solver.check() == sat
model = solver.model()
print("".join(chr(model.eval(code).as_long()) for code in codes))

Z3 ist ein Löser, der Werte findet, die diese Gleichungen erfüllen. Dieser Auszug verwendet die extrahierten Prüfungen und geht von einer DUCTF{…} flagge mit Buchstaben, Ziffern, Unterstrichen und geschweiften Klammern. Der vollständige Download enthält alle 26 Masken und Ziele.

Überprüfen Sie die Antwort mit dem Originalprogramm

Die Prozesserfassung von REA zeichnet die ursprüngliche ausführbare Datei auf, die das gelöste Flag akzeptiert. Ändern eines ausgewählten Zeichens aus z zu y macht die erste Summe 1440 anstelle von 1441, und das Programm lehnt sie ab.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Probieren Sie es selbst aus

Laden Sie die ursprüngliche Herausforderung und den Löser in einen Ordner herunter. Verwenden Sie die obige Eingabeaufforderung, um mit Ihrem Agenten Nachforschungen anzustellen, oder führen Sie das mitgelieferte Skript aus.

python3 -m venv .venv
.venv/bin/python -m pip install z3-solver
.venv/bin/python solve.py

chmod +x ms_flag_checker
./ms_flag_checker

Das Skript druckt ein Kandidatenflag; Fügen Sie es an der Eingabeaufforderung des Programms ein. Lösungsbedürfnisse Python und z3-solver. Zum Ausführen der ursprünglichen ausführbaren Datei ist Linux x86-64 erforderlich.