Найдите флаг в
двоичном формате 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.