Temukan bendera di
biner KKP.

Temukan kode pemeriksaan

Handout adalah executable 15 KB. Ia meminta bendera, lalu mencetak Correct! atau Incorrect!. Mulailah dengan permintaan sederhana kepada agen Anda.

Contoh prompt, dengan tantangan yang diunduh tersedia secara lokal dan analisis penyedia program kode mesin terhubung.

1. Ikuti prompt input ke fungsinya

   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 →

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

   Referensi memberi agen tempat untuk menyelidiki, meskipun nama fungsi asli yang dapat dieksekusi telah dihapus.

2. Baca pemeriksa dan dua pembantunya

   Agent → REA

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

   REA → agen * instruksi yang dipilih

   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

   Loop pertama menyalin 36 kode karakter. Loop pemeriksaan menerjemahkan topeng, menjumlahkan kode yang dipilih, dan membandingkan hasilnya dengan nomor yang disimpan. Nya 0x18- langkah byte melintasi 0x270 byte memberikan 26 topeng.

Ini adalah hasil yang dipilih dari analisis REA baru. Jalur target lokal dipersingkat untuk ditampilkan; alamat mengacu pada gambar yang diimpor REA.

Satu cek mengungkapkan satu karakter

Pemeriksa mengatur masukan dalam kisi 6× Topeng memilih sel mana yang berkontribusi pada penjumlahan. Pengkodeannya yang ringkas menggunakan angka negatif untuk melewati sel dan angka positif untuk memilihnya.

Baca topeng dan targetnya dari biner

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

Instruksi MOVSX membaca byte topeng sebagai nilai yang ditandatangani. Inilah mengapa eb artinya -21. Targetnya adalah bilangan bulat little-endian. Bersama-sama, byte ini memberi tahu agen bahwa code[21] = 55, jadi karakter itu adalah 7.

Dari instruksi hingga pemeriksaan yang dapat dibaca

Pilih langkah untuk menghubungkan summing helper dan fungsi pemanggilnya ke aturan yang sama di 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;
}

Instruksi datang dari pembantu penjumlahan dan fungsi pemanggilnya. C adalah ringkasan penjelasan dengan nama deskriptif dan loop 36 sel yang diratakan.

Selesaikan 26 persamaan tersebut

Sebagian besar topeng memilih beberapa sel. Misalnya, pemeriksaan pertama menambahkan 16 kode karakter dan membutuhkan total 1441. Pilihan yang tumpang tindih memberikan persamaan yang dapat diselesaikan bersama oleh skrip Python kecil.

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 adalah pemecah yang menemukan nilai-nilai yang memenuhi persamaan ini. Kutipan ini menggunakan pemeriksaan yang diekstraksi dan mengasumsikan DUCTF{…} bendera dengan huruf, angka,garis bawah, dan tanda kurung. Unduhan lengkap mencakup semua 26 topeng dan target.

Periksa jawabannya dengan program aslinya

Pengambilan proses REA merekam executable asli yang menerima flag yang diselesaikan. Mengubah satu karakter yang dipilih dari z untuk y membuat jumlah pertama 1440, bukan 1441, dan program menolaknya.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Cobalah sendiri

Unduh tantangan asli dan pemecah ke dalam satu folder. Gunakan perintah di atas untuk menyelidiki dengan agen Anda, atau jalankan skrip yang disertakan.

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

Skrip mencetak bendera kandidat; tempelkan pada prompt program. Memecahkan kebutuhan Python dan z3-solver. Menjalankan executable asli membutuhkan Linux x86-64.