Знайдіть прапор у
двійковому форматі CTF.

Знайдіть код підтвердження

Роздатковий матеріал являє собою виконуваний файл розміром 15 КБ. Він запитує прапорець, потім виводить "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 байт по 0x270 байт дають 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 зчитує байти маски як значення зі знаком. Ось чому eb означає -21. Метою є ціле число в порядку убування. Разом ці байти повідомляють агенту, що 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. Перекриваються вибірки дають рівняння, які може вирішити невеликий скрипт 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 записує оригінальний виконуваний файл, який приймає прапор solved. Зміна одного вибраного символу з z на y призводить до отримання першої суми 1440 замість 1441, і програма відхиляє її.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Спробуйте самі

Завантажте оригінальне завдання та рішення в одну папку. Скористайтеся наведеною вище інструкцією, щоб провести розслідування за допомогою свого агента, або запустіть доданий сценарій.

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

Сценарій виводить прапор кандидата; вставте його в командний рядок програми. Для вирішення потрібен Python і z3-solver. Для запуску оригінального виконуваного файлу потрібен Linux x86-64.