Trouvez le drapeau dans
un binaire CTF.

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.

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.

Lire le masque et sa cible à partir du binaire

{"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

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.

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;
}

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.

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.

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.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

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.

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.