--- title: 'CTF-Rückentwicklung: DownUnderCTF-Flaggenprüfer - REA' url: https://rea.tools/de/showcase/ctf/ --- [Startseite](https://rea.tools/de/) / [Präsentieren](https://rea.tools/de/showcase/) / CTF Fallstudie \* DownUnderCTF 2023 # Finde die Flagge in eine CTF-Binärdatei. Verwenden Sie REA, um einen kleinen Flaggenprüfer zu überprüfen, seine Regeln in Gleichungen umzuwandeln und eine Eingabe zu finden, die das ursprüngliche Programm drucken lässt `Correct!`. maskierte Quadrate Flaggenprüfer · Einfach · Linux x86-64 [Sehen Sie sich die ursprüngliche Herausforderung an](https://github.com/DownUnderCTF/Challenges_2023_Public/tree/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker) Von einer binären zu einer geprüften Antwort 1. 01 \* Finden Sie den Scheck **Zeichenketten → Funktionen prüfen** REA findet die Eingabeaufforderung, ihre Referenzen und den Code, der eine Eingabe akzeptiert oder ablehnt. 2. 02 \* Extrahieren Sie die Regeln **36 zeichen · 26 summen** REA gibt die Anweisungen und Daten hinter jeder Prüfung zurück. Der Agent wandelt sie in Gleichungen um. 3. 03 \* Lösen und ausführen **Wiederhergestellte Flagge → Korrekt!** Ein Python-Skript löst die Gleichungen. REA erfasst das ursprüngliche Programm, das das Ergebnis akzeptiert. Die Herausforderung stammt von Joseph und wurde im offiziellen Repository von DownUnderCTF veröffentlicht. ## 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. Ihr Codierungsagent Verwenden Sie REA, um ms_flag_checker zu analysieren und das Flag zu finden. Erklären Sie, wie die Prüfungen funktionieren, und überprüfen Sie dann die Antwort mit dem Originalprogramm. 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. ![Die siebte Maske überspringt 21 Zellen, wählt Position 21 aus und überspringt dann 14. Nur diese Zelle trägt zur Summe bei. Der erforderliche Zeichencode ist 55, was bedeutet, dass das Zeichen 7 ist.](https://rea.tools/assets/localized/de/figures/ctf-mask-equation.svg) Die siebte Prüfung wählt nur eine Position aus. [Offene Figur](https://rea.tools/assets/localized/de/figures/ctf-mask-equation.svg). ### Lesen Sie die Maske und ihr Ziel aus der Binärdatei Agent → REA · Byte lesen ``` {"address": "0x1040e0", "length": 624} {"address": "0x104060", "length": 144} ``` REA → Agent \* siebte Einträge ``` 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. REA \* ausgewählte Originalanleitung ``` 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 ``` Lesbare C · One-Check-Zusammenfassung ``` 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; } ``` **01 \* Bei Null beginnen.** `ECX` enthält die laufende Summe. **02 · Überprüfen Sie die Maskenzelle.** Ein Nullwert überspringt das Zeichen; Ein Wert ungleich Null schließt es ein. **03 \* Fügen Sie einen Zeichencode hinzu.** Die Ganzzahl der Eingabe am gleichen Offset wird zur Summe addiert. **04 \* Gehe zur nächsten Zelle.** Die ursprüngliche Schleife rückt vier Bytes pro Ganzzahl vor und besucht sechs Zeilen mit sechs Zellen. **05 · Mit dem gespeicherten Zielwert vergleichen.** Die aufrufende Funktion erhält die Summe in `EAX`. Bei einer Abweichung springt sie zu `Incorrect!`. 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. Python \* Löser Auszug ``` 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. [Laden Sie den vollständigen Solver herunter](https://rea.tools/showcase/ctf/solve.py) ## Ü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. | Eingang | Beobachteter Output | Ausstiegscode | | --- | --- | --- | | Flagge des Lösers | `Correct!` | 0 | | Ein Charakter wurde geändert | `Incorrect!` | 255 | Zeigen Sie das wiederhergestellte Flag und die erfasste Ausgabe an REA \* ursprüngliche Programmausgabe ``` What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa} Correct! ``` Der wiederhergestellte Wert stimmt auch mit dem Flag in den veröffentlichten Challenge-Metadaten der Organisatoren überein, das nach dem Lösen der Binärdatei überprüft wurde. Quelle, Zielidentität und Analysedetails Neue Analyse und zwei Prozesserfassungen am 8. Oktober 2026 mit REA 4.1.0 mit Ghidra 12.1.4 auf Linux x64. Die Binärdatei ist eine gestrippte x86-64 ELF, 15.248 Byte. Ursprüngliche ausführbare Datei \* SHA-256 ``` dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae ``` Die Zeichenfolgenreferenzen, Funktionen und Konstanten wurden überprüft, bevor die Quelle oder Lösung des Veranstalters gelesen wurde. Der Python-Solver und das Diagramm wurden aus diesen REA-Ergebnissen erstellt. [Vergleiche mit der Quelle des Veranstalters](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/src/ms_flag_checker.c) · [Metadaten und Flag abfragen](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/ctfcli.yaml) · [REA Hinweise zum Nachweis](https://github.com/morluto/rea/blob/main/website/evidence/ctf-masked-squares.md) ## 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. [Laden Sie die ursprüngliche Herausforderung herunter](https://raw.githubusercontent.com/DownUnderCTF/Challenges_2023_Public/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/publish/ms_flag_checker)[Löser herunterladen](https://rea.tools/showcase/ctf/solve.py) Terminal \* lösen und ausführen ``` 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. [Richten Sie REA mit Ihrem Codierungsagenten ein](https://rea.tools/get-started/)