--- title: 'Зворотна інженерія CTF: перевірка прапора DownUnderCTF-REA' url: https://rea.tools/uk/showcase/ctf/ --- [Головний](https://rea.tools/uk/) сторінка / [Вітрина](https://rea.tools/uk/showcase/) / CTF Тематичне дослідження \* DownUnderCTF 2023 # Знайдіть прапор у двійковому форматі CTF. Використовуйте REA для перевірки невеликого засобу перевірки прапорів, перетворіть його правила в рівняння та знайдіть вхідні дані, які `Correct!`. пристрій для перевірки прапорців в маскованих квадратах \* просте \* Linux x86-64 [Перегляньте оригінальну задачу](https://github.com/DownUnderCTF/Challenges_2023_Public/tree/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker) Від двійкового коду до перевіреної відповіді 1. 01 \* знайдіть рядки перевірки **→ функція** перевірки REA знаходить запит, посилання на нього і код, який приймає або відхиляє дані, що вводяться. 2. 02 \* витягніть правила **з 36 символів \* 26 Сум** REA повертає інструкції та дані, що стоять за кожною перевіркою. Агент перетворює їх у рівняння. 3. 03 \* Вирішіть і запустіть **відновлений прапор → виправити!** Рівняння вирішуються сценарієм Python. REA фіксує вихідну програму, яка приймає результат. Завдання написано Джозефом і опубліковано в офіційному сховищі DownUnderCTF. ## Знайдіть код підтвердження Роздатковий матеріал являє собою виконуваний файл розміром 15 КБ. Він запитує прапорець, потім виводить "`Correct!` або "`Incorrect!`. Почніть з простого запиту до свого агента. Ваш кодуючий агент Використовуйте REA для аналізу ms_flag_checker та пошуку прапора. Поясніть, як працюють перевірки, а потім перевірте відповідь за допомогою оригінальної програми. Приклад запиту із завантаженим завданням, доступним локально, та підключеним постачальником програм для аналізу машинного коду. 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. Маска визначає, які клітини беруть участь у сумі. Компактне кодування використовує негативні числа для пропуску комірок і позитивні числа для їх вибору. ![Сьома маска пропускає 21 клітинку, вибирає позицію 21, потім пропускає 14. Тільки ця комірка вносить свій внесок у суму. Її обов'язковий код-55, що означає, що символ дорівнює 7.](https://rea.tools/assets/localized/uk/figures/ctf-mask-equation.svg) При сьомій перевірці вибирається тільки одна позиція. [Відкрийте малюнок](https://rea.tools/assets/localized/uk/figures/ctf-mask-equation.svg). ### Порахуйте маску та її ціль із двійкового файлу Агент → REA \* прочитано_байт ``` {"address": "0x1040e0", "length": 624} {"address": "0x104060", "length": 144} ``` REA → агент \* сьомі записи ``` 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. REA \* вибрані оригінальні інструкції ``` 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 ``` Читабельний підсумок C \* one-check ``` 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; } ``` **01 \* почніть з нуля.** `ECX` містить поточну суму. **02 \* перевірте клітинку маски.** Нульове значення пропускає символ; ненульове значення включає його. **03 \* додайте символьний код.** До суми додається ціле число, отримане при введенні з тим же зміщенням. **04 \* перехід до наступної комірки.** Початковий цикл просувається по чотири байти на ціле число і відвідує шість рядків по шість комірок. **05 \* порівняти зі збереженим цільовим значенням.** Абонент отримує суму в `EAX`. Невідповідність стає `Incorrect!`. Інструкції надходять від помічника по підсумовуванню і викликає його пристрою. C - це пояснювальна записка з описовими назвами та згладженим циклом із 36 клітинок. ## Розв'яжіть 26 рівнянь У більшості масок вибирається кілька осередків. Наприклад, при першій перевірці додається 16 кодів символів, і потрібно в цілому 1441. Перекриваються вибірки дають рівняння, які може вирішити невеликий скрипт Python. Уривок з Python \* solver ``` 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 масок і цільових об'єктів. [Завантажте повний вирішувач](https://rea.tools/showcase/ctf/solve.py) ## Перевірте відповідь за допомогою оригінальної програми Програма захоплення процесу REA записує оригінальний виконуваний файл, який приймає прапор solved. Зміна одного вибраного символу з `z` на `y` призводить до отримання першої суми 1440 замість 1441, і програма відхиляє її. | Уведення | Спостережуваний результат | Код виходу | | --- | --- | --- | | Прапор вирішувача | `Correct!` | 0 | | Один персонаж змінено | `Incorrect!` | 255 | Відобразити відновлений прапор і захоплені вихідні дані REA \* вихідний програмний результат ``` What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa} Correct! ``` Відновлене значення також відповідає прапору в опублікованих організаторами метаданих задачі, який був перевірений після вирішення двійкової задачі. Ідентифікація джерела, цілі та деталі аналізу Новий аналіз та два записи процесів, опубліковані 8 жовтня 2026 року, використовуючи REA 4.1.0 та Ghidra 12.1.4 на Linux x64. Двійковий файл являє собою урізаний x86-64 ELF, об'ємом 15 248 байт. Оригінальний виконуваний файл \* SHA-256 ``` dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae ``` Посилання на рядки, функції та константи були перевірені перед читанням вихідного коду або рішення організаторів. На основі цих результатів REA було створено вирішувач Python та діаграму. [Порівняйте з джерелом, наданим організаторами](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/src/ms_flag_checker.c) · [Метадані та прапор конкурсу](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/ctfcli.yaml) · [Примітки до доказів REA](https://github.com/morluto/rea/blob/main/website/evidence/ctf-masked-squares.md) ## Спробуйте самі Завантажте оригінальне завдання та рішення в одну папку. Скористайтеся наведеною вище інструкцією, щоб провести розслідування за допомогою свого агента, або запустіть доданий сценарій. [Скачайте оригінальну гру challenge](https://raw.githubusercontent.com/DownUnderCTF/Challenges_2023_Public/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/publish/ms_flag_checker)[Завантажити вирішувач](https://rea.tools/showcase/ctf/solve.py) Термінал \* вирішити і запустити ``` 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. [Налаштуйте REA за допомогою агента кодування](https://rea.tools/get-started/)