Znajdź flagę w
binarny CTF.

Znajdź kod kontrolny

Materiały informacyjne to plik wykonywalny o wielkości 15 KB. Prosi o flagę, a następnie drukuje Correct! lub Incorrect!. Zacznij od prostej prośby do swojego agenta.

Przykładowy monit z pobranym wyzwaniem dostępnym lokalnie i analizą podłączonego dostawcy programów kodu maszynowego.

1. Postępuj zgodnie z monitem wejściowym do jego funkcji

   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 * wybrane wyniki

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

   Odwołanie daje agentowi miejsce do zbadania, mimo że oryginalne nazwy funkcji pliku wykonywalnego zostały usunięte.

2. Przeczytaj kontroler i jego dwóch pomocników

   Agent → REA

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

   REA → agent * wybrane instrukcje

   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

   Pierwsza pętla kopiuje 36 kodów znaków. Pętla sprawdzania dekoduje maskę, sumuje wybrane kody i porównuje wynik z zapisaną liczbą. Jego 0x18- bajtowe kroki w poprzek 0x270 bajty dają 26 masek.

Są to wybrane wyniki ze świeżej analizy REA. Lokalna ścieżka docelowa jest skrócona do wyświetlania; adresy odnoszą się do importowanego obrazu REA.

Jeden czek ujawnia jedną postać

Kontroler układa dane wejściowe w siatce 6×6. Maska wybiera, które komórki przyczyniają się do sumy. Jego kompaktowe kodowanie wykorzystuje liczby ujemne do pomijania komórek i liczby dodatnie do ich wybierania.

Odczytaj maskę i jej cel z pliku binarnego

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

Instrukcja MOVSX odczytuje bajty maski jako wartości podpisane. Właśnie dlatego eb oznacza -21. Celem jest liczba całkowita little-endian. Razem te bajty mówią agentowi, że code[21] = 55, więc ta postać jest 7.

Od instrukcji do czytelnego czeku

Wybierz krok, aby połączyć pomocnika sumowania i jego wywołującego z tą samą regułą w 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;
}

Instrukcje pochodzą od pomocnika sumującego i jego dzwoniącego. C jest podsumowaniem wyjaśniającym z opisowymi nazwami i spłaszczoną pętlą 36 komórek.

Rozwiąż 26 równań

Większość masek wybiera kilka komórek. Na przykład pierwsze sprawdzenie dodaje 16 kodów znaków i wymaga łącznie 1441. Nakładające się zaznaczenia dają równania, które mały skrypt Pythona może rozwiązać razem.

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 to solver, który znajduje wartości spełniające te równania. Ten fragment wykorzystuje wyodrębnione kontrole i zakłada DUCTF{…} flaga z literami, cyframi, podkreśleniami i nawiasami klamrowymi. Pełne pobieranie obejmuje wszystkie 26 masek i celów.

Sprawdź odpowiedź za pomocą oryginalnego programu

REA przechwytywanie procesu rejestruje oryginalny plik wykonywalny akceptujący rozwiązaną flagę. Zmiana jednego wybranego znaku z z do y tworzy pierwszą sumę 1440 zamiast 1441, a program ją odrzuca.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Spróbuj sam

Pobierz oryginalne wyzwanie i solver do jednego folderu. Użyj powyższego monitu, aby zbadać sprawę z agentem lub uruchom dołączony skrypt.

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

Skrypt drukuje flagę kandydata; wklej go w monicie programu. Rozwiązywanie potrzeb Python i z3-solver. Uruchomienie oryginalnego pliku wykonywalnego wymaga Linux x86-64.