Trova la bandiera in
un binario CTF.

Trova il codice di controllo

Il volantino è un eseguibile da 15 KB. Chiede una bandiera, poi stampa Correct! o Incorrect!. Inizia con una semplice richiesta al tuo agente.

Un prompt di esempio, con la sfida scaricata disponibile localmente e un'analisi del provider di programmi di codice macchina collegato.

1. Seguire il prompt di input per la sua funzione

   Agente → 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 → agente * risultati selezionati

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

   Il riferimento fornisce all'agente un posto in cui indagare, anche se i nomi delle funzioni originali dell'eseguibile sono stati rimossi.

2. Leggi il correttore e i suoi due aiutanti

   Agente → REA

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

   REA → agente * istruzioni selezionate

   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

   Il primo ciclo copia 36 codici di caratteri. Il ciclo di controllo decodifica una maschera, somma i codici selezionati e confronta il risultato con un numero memorizzato. Sua 0x18- passi byte attraverso 0x270 i byte danno 26 maschere.

Questi sono risultati selezionati da una nuova analisi REA. Il percorso di destinazione locale viene abbreviato per la visualizzazione; gli indirizzi si riferiscono all'immagine importata di REA.

Un controllo rivela un carattere

Il controllore organizza l'ingresso in una griglia 6×6. Una maschera sceglie quali cellule contribuiscono a una somma. La sua codifica compatta utilizza numeri negativi per saltare le celle e numeri positivi per selezionarli.

Leggi la maschera e il suo obiettivo dal binario

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

Istruzione MOVSX legge i byte della maschera come valori firmati. Ecco perché eb significa -21. L'obiettivo è un numero intero little-endian. Insieme, questi byte dicono all'agente che code[21] = 55, in modo che il carattere è 7.

Dalle istruzioni a un controllo leggibile

Selezionare un passaggio per collegare l'helper sommatore e il suo chiamante alla stessa regola in 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;
}

Le istruzioni provengono dall'helper sommatore e dal suo chiamante. La C è un riassunto esplicativo con nomi descrittivi e un ciclo appiattito a 36 celle.

Risolvi le 26 equazioni

La maggior parte delle maschere seleziona diverse celle. Ad esempio, il primo controllo aggiunge 16 codici di caratteri e richiede un totale di 1441. Le selezioni sovrapposte danno equazioni che un piccolo script Python può risolvere insieme.

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 è un risolutore che trova valori che soddisfano queste equazioni. Questo estratto utilizza i controlli estratti e presuppone un DUCTF{…} bandiera con lettere, cifre, caratteri di sottolineatura e parentesi graffe. Il download completo include tutte le 26 maschere e obiettivi.

Controlla la risposta con il programma originale

L'acquisizione del processo di REA registra l'eseguibile originale accettando il flag risolto. Modifica di un carattere selezionato da z per y fa la prima somma 1440 invece di 1441, e il programma lo rifiuta.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Provalo tu stesso

Scarica la sfida originale e il risolutore in un'unica cartella. Utilizzare il prompt sopra per indagare con il proprio agente o eseguire lo script incluso.

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

Lo script stampa un flag candidato; incollarlo al prompt del programma. Risolvere i bisogni di Python e z3-solver. L'esecuzione dell'eseguibile originale richiede Linux x86-64.