Βρείτε τη σημαία σε
ένα δυαδικό αρχείο CTF.

Βρείτε τον κώδικα ελέγχου

Το παρεχόμενο αρχείο είναι ένα εκτελέσιμο 15 KB. Ζητά μια σημαία και έπειτα τυπώνει Correct! ή Incorrect!. Ξεκινήστε με ένα απλό αίτημα προς τον βοηθό σας.

Παράδειγμα προτροπής, με την πρόκληση που κατεβάσατε διαθέσιμη τοπικά και συνδεδεμένο πάροχο ανάλυσης κώδικα μηχανής.

1. Ακολουθήστε την προτροπή εισόδου μέχρι τη συνάρτησή της

   Βοηθός → 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 → βοηθός · επιλεγμένα αποτελέσματα

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

   Η αναφορά δίνει στον βοηθό ένα σημείο για διερεύνηση, παρότι τα αρχικά ονόματα συναρτήσεων του εκτελέσιμου έχουν αφαιρεθεί.

2. Διαβάστε το πρόγραμμα ελέγχου και τις δύο βοηθητικές συναρτήσεις του

   Βοηθός → REA

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

   REA → βοηθός · επιλεγμένες εντολές

   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

   Ο πρώτος βρόχος αντιγράφει 36 κωδικούς χαρακτήρων. Ο βρόχος ελέγχου αποκωδικοποιεί μια μάσκα, αθροίζει τους επιλεγμένους κωδικούς και συγκρίνει το αποτέλεσμα με έναν αποθηκευμένο αριθμό. Τα βήματα των 0x18 byte σε 0x270 byte δίνουν 26 μάσκες.

Αυτά είναι επιλεγμένα αποτελέσματα από νέα ανάλυση του REA. Η τοπική διαδρομή του στόχου συντομεύεται για την εμφάνιση· οι διευθύνσεις αναφέρονται στην εικόνα που εισήγαγε το REA.

Ένας έλεγχος αποκαλύπτει έναν χαρακτήρα

Το πρόγραμμα ελέγχου τοποθετεί την είσοδο σε πλέγμα 6×6. Μια μάσκα επιλέγει ποια κελιά συνεισφέρουν σε ένα άθροισμα. Η συμπαγής κωδικοποίησή της χρησιμοποιεί αρνητικούς αριθμούς για να παραλείπει κελιά και θετικούς για να τα επιλέγει.

Διαβάστε τη μάσκα και την τιμή-στόχο της από το δυαδικό αρχείο

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

Η εντολή MOVSX διαβάζει τα byte της μάσκας ως προσημασμένες τιμές. Γι' αυτό το eb σημαίνει −21. Η τιμή-στόχος είναι ακέραιος little-endian. Μαζί, αυτά τα byte λένε στον βοηθό ότι code[21] = 55, άρα ο χαρακτήρας είναι 7.

Από τις εντολές σε έναν ευανάγνωστο έλεγχο

Επιλέξτε ένα βήμα για να συνδέσετε τη βοηθητική συνάρτηση αθροίσματος και τον καλούντα της με τον ίδιο κανόνα σε 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;
}

Οι εντολές προέρχονται από τη βοηθητική συνάρτηση αθροίσματος και τον καλούντα της. Ο κώδικας C είναι μια επεξηγηματική σύνοψη με περιγραφικά ονόματα και έναν ενιαίο βρόχο 36 κελιών.

Λύστε τις 26 εξισώσεις

Οι περισσότερες μάσκες επιλέγουν πολλά κελιά. Για παράδειγμα, ο πρώτος έλεγχος προσθέτει 16 κωδικούς χαρακτήρων και απαιτεί σύνολο 1441. Οι αλληλεπικαλυπτόμενες επιλογές δίνουν εξισώσεις που ένα μικρό script 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 είναι ένας λύτης που βρίσκει τιμές οι οποίες ικανοποιούν αυτές τις εξισώσεις. Αυτό το απόσπασμα χρησιμοποιεί τους εξαγόμενους ελέγχους και υποθέτει μια σημαία DUCTF{…} με γράμματα, ψηφία, κάτω παύλες και άγκιστρα. Το πλήρες αρχείο λήψης περιλαμβάνει και τις 26 μάσκες και τιμές-στόχους.

Ελέγξτε την απάντηση με το αρχικό πρόγραμμα

Η καταγραφή διεργασίας του REA καταγράφει την αποδοχή της σημαίας που βρέθηκε από το αρχικό εκτελέσιμο. Η αλλαγή ενός επιλεγμένου χαρακτήρα από z σε y κάνει το πρώτο άθροισμα 1440 αντί για 1441 και το πρόγραμμα το απορρίπτει.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Δοκιμάστε το μόνοι σας

Κατεβάστε την αρχική πρόκληση και τον λύτη σε έναν φάκελο. Χρησιμοποιήστε την παραπάνω προτροπή για να διερευνήσετε με τον βοηθό σας ή εκτελέστε το παρεχόμενο script.

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

Το script τυπώνει μια υποψήφια σημαία· επικολλήστε τη στην προτροπή του προγράμματος. Η επίλυση απαιτεί Python και z3-solver. Η εκτέλεση του αρχικού εκτελέσιμου απαιτεί Linux x86-64.