Решение promix17 - MazeJumps

Сложность: 3 - Getting harder
Платформа: Windows
Язык: Assembler
Дано: MazeJumps

MazeJumps v1.0
Written by Promix17
Цель – зарегистрировать программу с помощью key-файла.
Этот crackme имеет необычную структуру кода. Надеюсь, она вам понравится.
Удачи)))

Решение (автор ForFun, bike, zairon)
опубликовано 09.01.2013

Инструмент: IDA

При статическом анализе crackme обращаем внимание на малое количество импортируемых функций.
image00.jpg

Т.к. наша цель – найти файл, то ставим точку останова на функцию открытия файла CreateFileA. Как только точка останова срабатывает, то увидим, что функция ожидает «key.txt» файл. Что ж, создаем его (в том же каталоге, где и crackme), вводим несколько символов, и перезапускаем программу. Но тут возникает другая проблема - crackme обфусцирован: код перемешан с кучей мусорных инструкций и безусловных переходов (jmp). Поэтому, чтобы вникнуть в алгоритм защиты нам потребуется деобфускатор.

1. Деобфускатор

Итак, мусорный код. Излюбленный способ всевозможных защит и вирусов усложнить анализ для реверсера. Посмотрим, как выглядит такой код в нашей задаче:

image01.jpg

Много (очень много) jmp-инструкций и много «бестолковых» команд. Реальная проблема заключается в определении правильных инструкций, связанных с работой и логикой crackme. Тут два варианта действий:
1. выполнять код crackme под отладчиком пошагово, пытаясь определить правильные и не правильные инструкции
2. каким-то образом автоматизировать деобфускацию crackme

Вариант 1 представляет собой самый простой и утомительный способ, потому что вы обязательно найдете правильную инструкцию, анализируя код команду за командой. В данном случае это хороший подход, ибо весь код задачки весит только 35КБайт … Но сколько придется потратить нервов и сил в случае анализа большого обфусцированного файла? Вот почему я выбираю вариант 2!

Я думаю, что второй вариант не имеет универсального решения. Написание деобфускатора чаще всего индивидуально для каждой программы и, по сути, всегда вызов для реверсера. Каждый раз анализируется конкретная реализация обфускатора. В нашем случае нам надо избавиться от jmp-хлама и «мусорных» инструкций.

Самая раздражающая вещь в нашем crackme – вездесущие безусловные переходы (JMP). Повторюсь - их много, очень много. Через каждые три-пять инструкций встречаем JMP-переход. Попытка просмотреть такой код в дизассемблере, кроме головной боли ничего не вызывает. В этом случае простой способ деобфускации: пройтись по коду, эмулируя и отбрасывая все инструкции JMP. За основу я взял решение, опубликованное в блоге http://hooked-on-mnemonics.blogspot.ru/2012/10/simple-deobfuscation-of-code.html, а именно рекурсивный алгоритм дизассемблирования (recursive traversal disassembler - http://ftp.cs.arizona.edu/~debray/Publications/disasm.pdf ).

Псевдокод рекурсивного алгоритма дизассемблирования:



Есть еще один нюанс. Программа иногда совершает неявный jmp-переход. На ассемблере это выглядит как пара команд:
push адрес

ret
В этом случае мы запускаем отладчик, ставим точку останова на ret, запускаем программу и узнаем адрес следующей инструкции. Как выяснилось, таких ситуаций в коде возникает три раза:
Деобфускатор (0x401000)
Деобфускатор (0x40812F)
Деобфускатор (0x405ADD)

Рекурсивный алгоритм дизассемблирования будем писать на Python’е и выполнять в IDA, используя плагин IDAPython.
Результат работы скрипта:

image02.jpg

2. Алгоритм защиты.

Когда мы изучим алгоритм, то увидим, что он проверяет первые три 32-битных слова (DWORD) ключа. Третий DWORD сравнивается напрямую и должен быть равен 0x21643172 или как ASCII-строка «r1d!» (сравнение по адресу 0x40602A). Обозначим k0 и k1 как первый и второй DWORD. Тогда проверочные выражения такие:
(k0 XOR a1) + (k1 XOR b1) = c1 (1)
(k0 XOR a2) + (k1 XOR b2) = c2 (2),
где a1, b1, c1, a2, b2, c2 – константы, задаваемые в коде; а сложение происходит по модулю 232

Значит, чтобы найти k0 и k1, нам без брутфорса не обойтись. Попробуем… И выясняется - у нас проблема, которая заключается в том, что существует множество вариантов для значений k0 и k1, удовлетворяющих условиям (1) и (2). Можно добавить условие, что k0 и k1 должны состоять из букв и цифр (0..9a..zA..Z и пробела). Даже в этом случае, по-прежнему, слишком много решений. Но посмотрите, в конце кода вызывается функция MessageBoxA. Текст, который она отображает, состоит из 8 байт:
первые четыре байта - k0 XOR a3 (3)
следующие четыре байта - k1 XOR b3 (4),
где a3, b3 – константы

Можно предположить, что этот текст цифро-буквенный, заканчивающийся нулем. Добавляем эти условия для нашего брутфорса и получаем только два правильных ключа.
Ключ: Hello wor1d! Сообщение для MessageBoxA: Success
Ключ: Jellm wor1d! Сообщение для MessageBoxA: Quccgss

Угадайте, какой более правильный :)

Наш брутфорс мы оформим как выражение для пакета Z3 An Efficient Theorem Prover («решатель теорем») от Microsoft Research. Как ни странно, в последнее время Z3 используют как удобное средство для кейгена ряда алгоритмов. Библиотека Z3 бесплатна, после установки пакета Z3 достаточно положить в папку с нашим скриптом файлы: z3.dll, z3*.py (z3.py, z3consts.py, z3core.py, …). Рассмотрим код для кейгена:

Кстати, выражения можно решать и онлайн. Краткая ссылка брутфорса http://rise4fun.com/Z3Py/zEP2t.
А теперь смотрим код с комментариями.

# -*- coding: cp1251 -*-
from z3 import *
 
# добавить условие: символ должен попадать в алфавит
def isalpha(s, ch, alpha_l):
    sub_eq = False
    for i in alpha_l:
        sub_eq = Or(sub_eq, ch == i)
    s.append(sub_eq)
 
# наш алфавит
alpha = " abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
alpha_l = []
for i in alpha:
    alpha_l.append(ord(i))
 
# константы из crackme
a1 = 0xF45A675D
b1 = 0x4DDAFA31
c1 = 0xBAE3DC73
a2 = 0xAADD357D
b2 = 0x44FAFC3C
c2 = 0xF23F2C88
 
# создаем объект Solver библиотеки Z3
solver = Solver()
 
# создаем переменные, которые должны найти
# k0 и k1 - DWORD (32 бита)
key = []
for i in xrange(2) :
    key.append(BitVec("k%d"%i, 32))
 
# пишем выражение:
# условие (1)
check1 = (key[0] ^ a1) + (key[1] ^ b1)
# условие (2)
check2 = (key[0] ^ a2) + (key[1] ^ b2)
# условие (3)
mes1 = key[0] ^ 0xF0F101B;
# условие (4)
mes2 = key[1] ^ 0x6F04530A;
solver.append(check1 == c1, check2 == c2)
 
# k0 - это DWORD, байты ключа должны попадать в алфавит
isalpha(solver, key[0] & 0xFF, alpha_l)
isalpha(solver, (key[0] >> 8) & 0xFF, alpha_l)
isalpha(solver, (key[0] >> 16) & 0xFF, alpha_l)
isalpha(solver, (key[0] >> 24) & 0xFF, alpha_l)
 
# k01- это DWORD, байты ключа должны попадать в алфавит
isalpha(solver, key[1] & 0xFF, alpha_l)
isalpha(solver, (key[1] >> 8) & 0xFF, alpha_l)
isalpha(solver, (key[1] >> 16) & 0xFF, alpha_l)
isalpha(solver, (key[1] >> 24) & 0xFF, alpha_l)
 
# mes1 - это текст (первые 4 байта) для MessageBoxA
isalpha(solver, mes1 & 0xFF, alpha_l)
isalpha(solver, (mes1 >> 8) & 0xFF, alpha_l)
isalpha(solver, (mes1 >> 16) & 0xFF, alpha_l)
isalpha(solver, (mes1 >> 24) & 0xFF, alpha_l)
 
# mes2 - это текст (следующие 4 байта) для MessageBoxA
isalpha(solver, mes2 & 0xFF, alpha_l)
isalpha(solver, (mes2 >> 8) & 0xFF, alpha_l)
isalpha(solver, (mes2 >> 16) & 0xFF, alpha_l)
# самый младший байт должен быть равен 0 (завершающий байт текста)
nilbyte = (mes2 >> 24) & 0xFF
solver.append(nilbyte == 0)
 
# запускаем расчет с перебором всех решений
while solver.check() == sat:
    # нашли одно решение
    solution = solver.model()
    # k0, k1 преобразуем в строку
    str_x = ""
    x = int(str(solution[key[0]]))
    str_x = chr(x & 0xFF)+chr((x >> 8) & 0xFF)+chr((x >> 16) & 0xFF)+chr((x >> 24) & 0xFF)
    x = int(str(solution[key[1]]))
    str_x += chr(x & 0xFF)+chr((x >> 8) & 0xFF)+chr((x >> 16) & 0xFF)+chr((x >> 24) & 0xFF)
    # вывод на печать
    print ("Key: "+str_x)
 
    # задаем условие, чтобы найти следующее решение
    solver.add(Or(key[0] != solution[key[0]], key[1] != solution[key[1]]))


Результат. Создаем «key.txt» со строкой «Hello wor1d!» и запускаем программу.

image03.jpg
Пока не указано иное, содержимое этой страницы распространяется по лицензии Creative Commons Attribution-ShareAlike 3.0 License