--- title: 'Ingénierie inverse CTF: Vérificateur de drapeau DownUnderCTF-REA' url: https://rea.tools/fr/showcase/ctf/ --- [Accueil](https://rea.tools/fr/) / [Vitrines](https://rea.tools/fr/showcase/) / FCT Étude de cas \* DownUnderCTF 2023 # Trouvez le drapeau dans un binaire CTF. Utilisez REA pour inspecter un petit vérificateur d'indicateurs, transformer ses règles en équations et trouver une entrée qui fait imprimer le programme d'origine `Correct!`. vérificateur de drapeau carrés masqués \* Facile \* Linux x86-64 [Voir le défi original](https://github.com/DownUnderCTF/Challenges_2023_Public/tree/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker) D'une réponse binaire à une réponse vérifiée 1. 01 \* Trouver le chèque **Chaînes → fonctions de vérification** REA trouve l'invite, ses références et le code qui accepte ou rejette une entrée. 2. 02 \* Extraire les règles **36 caractères · 26 sommes** REA renvoie les instructions et les données derrière chaque vérification. L'agent les transforme en équations. 3. 03 \* Résoudre et exécuter **Drapeau récupéré → Correct!** Un script Python résout les équations. REA capture le programme d'origine acceptant le résultat. Le défi est de joseph, publié dans le référentiel officiel de DownUnderCTF. ## Trouver le code de vérification Le document est un exécutable de 15 Ko. Il demande un drapeau, puis imprime `Correct!` ou `Incorrect!`. Commencez par une simple demande à votre agent. Votre agent de codage Utilisez REA pour analyser ms_flag_checker et trouver l'indicateur. Expliquez le fonctionnement des vérifications, puis vérifiez la réponse avec le programme d'origine. Un exemple d'invite, avec le défi téléchargé disponible localement et une analyse du fournisseur de programmes en code machine connecté. 1. #### Suivez l'invite de saisie jusqu'à sa fonction Agent → 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 · résultats sélectionnés ``` 0x102004 "What is the flag? " 0x10201c "Incorrect!" 0x102027 "Correct!" Prompt referenced at: 0x10126d Containing function: 0x10124d ``` La référence donne à l'agent un endroit pour enquêter, même si les noms de fonctions d'origine de l'exécutable ont été supprimés. 2. #### Lire le vérificateur et ses deux aides Agent → REA ``` analyze_function {"procedure": "0x10124d"} analyze_function {"procedure": "0x101189"} analyze_function {"procedure": "0x101217"} ``` REA → agent \* instructions sélectionnées ``` 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 ``` La première boucle copie 36 codes de caractères. La boucle de contrôle décode un masque, additionne les codes sélectionnés et compare le résultat avec un nombre stocké. Ses `0x18`- étapes d'octets à travers `0x270` les octets donnent 26 masques. Ce sont des résultats sélectionnés à partir d'une nouvelle analyse REA. Le chemin cible local est raccourci pour l'affichage; les adresses se réfèrent à l'image importée de REA. ## Un chèque révèle un caractère Le vérificateur organise l'entrée dans une grille 6×6. Un masque choisit quelles cellules contribuent à une somme. Son codage compact utilise des nombres négatifs pour sauter les cellules et des nombres positifs pour les sélectionner. ![Le septième masque saute 21 cellules, sélectionne la position 21, puis saute 14. Seule cette cellule contribue à la somme. Son code de caractère requis est 55, ce qui signifie que le caractère est 7.](https://rea.tools/assets/localized/fr/figures/ctf-mask-equation.svg) La septième vérification sélectionne une seule position. [Figure ouverte](https://rea.tools/assets/localized/fr/figures/ctf-mask-equation.svg). ### Lire le masque et sa cible à partir du binaire Agent → REA \* lire_octets ``` {"address": "0x1040e0", "length": 624} {"address": "0x104060", "length": 144} ``` REA → agent \* septième entrées ``` Mask at 0x104170: eb 01 f2 00 → -21, +1, -14, stop Target at 0x104078: 37 00 00 00 → 55 ``` L'instruction `MOVSX` lit les octets du masque en tant que valeurs signées. C'est pourquoi `eb` signifie -21. La cible est un entier little-endian. Ensemble, ces octets indiquent à l'agent que `code[21] = 55`, donc ce personnage est `7`. ## Des instructions à un chèque lisible Sélectionnez une étape pour connecter l'assistant de sommation et son appelant à la même règle en C. REA \* instructions d'origine sélectionnées ``` 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 ``` Résumé lisible de C \* one-check ``` 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 \* Commencez à zéro.** `ECX` détient la somme courante. **02 \* Vérifiez la cellule du masque.** Une valeur nulle ignore le caractère; une valeur différente de zéro l'inclut. **03 \* Ajouter un code de caractère.** L'entier de l'entrée au même décalage est ajouté à la somme. **04 \* Passez à la cellule suivante.** La boucle d'origine avance de quatre octets par entier et visite six rangées de six cellules. **05 \* Comparer avec la cible stockée.** L'appelant reçoit la somme en `EAX`. Un décalage saute à `Incorrect!`. Les instructions proviennent de l'assistant de sommation et de son appelant. Le C est un résumé explicatif avec des noms descriptifs et une boucle aplatie de 36 cellules. ## Résoudre les 26 équations La plupart des masques sélectionnent plusieurs cellules. Par exemple, la première vérification ajoute 16 codes de caractères et nécessite un total de 1441. Les sélections qui se chevauchent donnent des équations qu'un petit script Python peut résoudre ensemble. Extrait du solveur Python · ``` 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 est un solveur qui trouve des valeurs satisfaisant ces équations. Cet extrait utilise les vérifications extraites et suppose une `DUCTF{…}` drapeau avec des lettres, des chiffres, des traits de soulignement et des accolades. Le téléchargement complet comprend les 26 masques et cibles. [Télécharger le solveur complet](https://rea.tools/showcase/ctf/solve.py) ## Vérifiez la réponse avec le programme d'origine La capture de processus de REA enregistre l'exécutable d'origine acceptant l'indicateur résolu. Changer un caractère sélectionné à partir de `z` à `y` fait la première somme 1440 au lieu de 1441, et le programme la rejette. | Entrée | Production observée | Code de sortie | | --- | --- | --- | | Drapeau du solveur | `Correct!` | 0 | | Un personnage a changé | `Incorrect!` | 255 | Afficher l'indicateur récupéré et la sortie capturée REA \* sortie du programme d'origine ``` What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa} Correct! ``` La valeur récupérée correspond également au drapeau dans les métadonnées de défi publiées par les organisateurs, vérifiées après la résolution du binaire. Détails de la source, de l'identité de la cible et de l'analyse Nouvelle analyse et deux captures de processus le 8 octobre 2026, en utilisant REA 4.1.0 avec Ghidra 12.1.4 sur Linux x64. Le binaire est un ELF x86-64 dépouillé, 15 248 octets. Fichier exécutable d'origine \* SHA-256 ``` dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae ``` Les références de chaîne, les fonctions et les constantes ont été inspectées avant de lire la source ou la solution des organisateurs. Le solveur Python et le diagramme ont été construits à partir de ces résultats REA. [Comparez avec la source des organisateurs](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/src/ms_flag_checker.c) · [Contester les métadonnées et l'indicateur](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/ctfcli.yaml) · [REA notes de preuve](https://github.com/morluto/rea/blob/main/website/evidence/ctf-masked-squares.md) ## Essayez-le vous-même Téléchargez le défi d'origine et le solveur dans un seul dossier. Utilisez l'invite ci-dessus pour enquêter avec votre agent ou exécutez le script inclus. [Télécharger le défi original](https://raw.githubusercontent.com/DownUnderCTF/Challenges_2023_Public/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/publish/ms_flag_checker)[Télécharger le solveur](https://rea.tools/showcase/ctf/solve.py) Terminal \* résoudre et exécuter ``` 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 ``` Le script imprime un drapeau candidat; collez-le à l'invite du programme. La résolution des besoins Python et `z3-solver`. L'exécution de l'exécutable d'origine nécessite Linux x86-64. [Configurez REA avec votre agent de codage](https://rea.tools/get-started/)