Недавно Microsoft опубликовала свой SMT-решатель Z3. Давай попробуем разобраться, как можно применить этот инструмент в практических целях.

 

Intro

Сначала определимся с терминами и областью применения. SMT — это теоремы специального вида, решаемые в конечных полях. Поскольку вся булева арифметика, используемая в компьютерах, является арифметикой в конечном поле, SMT хорошо подходит для описания программ. При помощи таких теорем можно представить задачу crackme или условия, при которых реализуется уязвимость в ПО.

До публикации использовать Z3 было довольно неудобно. Приходилось учить новый язык, а запустить решатель можно было только на сайте (кстати, там же находится tutorial для тех, кто хочет выучить сам язык). Сейчас Z3 можно запустить на своем компьютере, и к нему теперь доступны различные API (C, C++, .NET, Java, Python), из которых мы будем использовать Z3Py — API для Python.

 

Устанавливаем Z3

Начнем с установки. Любителям винды придется скачать Z3 с сайта, установить и добавить поддиректорию z3/bin в переменные среды PATH и PYTHONPATH. Линуксоидам нужно выполнить следующие команды:

mkdir z3
cd z3
git clone https://github.com/Z3Prover/z3
cd z3
python scripts/mk_make.py
cd build
make
sudo make install

Локальную документацию генерируем так:

sudo apt-get install doxygen
cd doc
python mk_api_doc.py

Документацию можно просмотреть, открыв файл doc/api/html/index.html.
Проверим, все ли правильно установилось. Создаем файл z3example.py cо следующим кодом:

from z3 import *

def Check():
  a = BitVec('a',32)
  b = BitVecVal(0xdeaddead,32)
  c = BitVecVal(0xbeefbeef,32)
  s=Solver()
  s.add(LShR(b,2)^a==c)
  if s.check()==sat:
    print "Equation satisfiable"
    print "0x%8X"%s.model()[a].as_long()
    return
  print "Equation unsatisfiable"

if __name__=="__main__":
  Check()

Запускаем:

python z3example.py
 

Осваиваем Z3

Если все установилось правильно, то программа должна вывести:

Equation satisfiable
0x8944C944

Что делает этот код? Сначала мы создаем переменную а размером 32 бита, значение которой мы хотим найти. Далее мы создаем две константы соответствующего размера. Потом мы инициализируем решатель. При помощи метода add добавляем в решатель правило: (b>>2)^a=c. Метод check запускает решатель и возвращает значение sat в случае, если решение найдено. Метод model возвращает модель со значениями, удовлетворяющими условию. Модель представляет собой хеш-таблицу, из которой можно получить значение каждой переменной, переданной в решатель.

Z3 поддерживает типы Bool, Int, BitVec, Array, Real, FP (floating point). Типы Bool, Real и Int соответствуют своим названиям. Тип BitVec — это по сути беззнаковое число с определяемым в битах размером. Тип Array позволяет определить типы индексатора и элементов, FP — задать количество битов под экспоненту и мантиссу.

Примеры инициализации:

a = Bool('a')
b=Int('b')
c=Real('c')
d=BitVec('d',32)
e=Array('e',IntSort(),BoolSort())
f=FP('f',FPSort(8,24))

Что такое Sort? Так в Z3 называется тип. Очевидно, IntSort() возвращает тип Int, BoolSort() тип Bool и так далее. Узнать тип переменной можно при помощи метода sort. Например:

python
>>> from z3 import *
>>> a= Int('a')
>>> b= Real('b')
>>> (a+b).sort()
Real

Для типа FP существуют наследственные типы с определенными размерами (Float16/FloatHalf, Float32/FloatSingle, Float64, Float128).

Все типы, кроме Array, можно определять сразу для нескольких переменных. Достаточно добавить к методу суффикс s:

>>> a, b = BitVecs('a b',16)

Для всех типов, кроме Array, можно создавать константы. Чтобы инициализировать константу, достаточно добавить к имени типа слово Val и передать ей необходимое значение в качестве первого аргумента. Например:

>>> b=BitVecVal(0x1, 32)

Для всех типов, кроме BitVec и Array, можно использовать константы без инициализации:

>>> a=Int('a')
>>> s=Solver()
>>> s.add(a==1)

Константы типа Real можно инициализировать рациональными числами. При этом дробное представление сохранится.
Z3 также позволяет создавать функции.

>>> from z3 import *
>>> f = Function('f', IntSort(), IntSort(), BoolSort())
>>> a=Int('a')
>>> b=Int('b')
>>> s=Solver()
>>> s.add(ForAll([a,b],f(a,b)==(a==b)))
>>> x=Int('x')
>>> y=IntVal(0x10)
>>> s.add(f(x,y)==BoolVal(True))
>>> if s.check()==sat:
...             print s.model()[x]
...
16

Метод ForAll позволяет определить значение функции для всех возможных значений аргумента. Функцию можно определить для отдельных аргументов, тогда Z3 попробует определить функцию для всех значений:

>>> from z3 import *
>>> f=Function('f',IntSort(),IntSort(),BoolSort())
>>> s=Solver()
>>> s.add(f(0,1)==False)
>>> s.add(f(1,1)==True,f(1,0)==False,f(0,0)==True)
>>> if s.check()==sat:
...     print s.model()[f]
...
[(0, 1) -> False,
 (1, 1) -> True,
 (1, 0) -> False,
 (0, 0) -> True,
 else -> False]

Для повторения логики программы лучше всего использовать тип BitVec, при помощи которого удобно эмулировать операции с регистрами. Он поддерживает битовые сдвиги, вращение, операции и, или и исключающее или. У него есть одна особенность, из-за которой программа может не найти решение твоей проблемы. Операция >> определена в Z3Py не как логический сдвиг, а как арифметический, то есть с переносом значения флага carry в верхний разряд. Для логического сдвига нужно использовать метод LShR. Для операций битового вращения (rol, ror) есть методы RotateLeft и RotateRight.

Напишем простую программу с этими операциями:

from z3 import *

def Check():
  a,b,c =BitVecs('a b c',32)
  s=Solver()
  s.add(RotateLeft(a^b,48)==(RotateRight(c,8)&BitVecVal(0x3457ac24,32)))
  s.add(a&b&c!=BitVecVal(0,32))
  if s.check()==sat:
  m=s.model()
  print '0x%0.8X'%m[a].as_long()
  print '0x%0.8X'%m[b].as_long()
  print '0x%0.8X'%m[c].as_long()

if __name__=='__main__':
  Check()

Тип BitVec можно представить в качестве знакового или беззнакового числа при помощи методов as_signed_long и as_long соответственно. Если нужно перевести тип BitVec в Int внутри решателя, поможет процедура BV2Int. Кстати, в нашем коде использовалась процедура RotateLeft со вторым аргументом 48 при размере вектора 32. Очевидно, его можно упростить. Решатель Z3 делает это автоматически, но можно упростить код и самому при помощи процедуры simplify:

>>>from z3 import *
>>> a,b = Ints('a b')
>>>simplify((a+1)*(b+3),som=True)
3 +3*a + b + a*b

som — это опция, раскладывающая сложные произведения в сумму. Чтобы просмотреть все параметры функции simplify, необходимо вызвать функцию help_simplify().

Z3 позволяет использовать методы питона в качестве уравнений, что очень удобно, если код, который ты попытаешься представить при помощи SMT, использует циклы. Функция должна возвращать True, False или тип Z3 Bool. На вход ей должны быть переданы только аргументы типов Z3. Например:

from z3 import *

def f1(a):
  b=0x12345678
  c=0x23874816
  d=0x42146789
  return (a^b)==(c^d)

def c1(a):
  b=0x1
  i=0
  while i<10:
    b=b+i
    i=i+1
  return a==b

def Check():
  s=Solver()
  a,b,c=BitVecs('a b c',32)
  s.add(c1(a))
  s.add(f1(b))
  s.add(a^b==c)
  if s.check()==sat:
    print 'Satisfiable'
    print s.model()

if __name__=='__main__':
  Check()

Исполняем:

python z3MethodExample.py
Satisfiable
[b = 1940355559, c = 19403555529, a = 46]
 

Ломаем тестовый кракми

При решении crackme удобно использовать сразу несколько функций. Например, в одной реализовать проверку на символы английского алфавита, а в другой логику самого crackme. Допустим, у нас есть такой crackme:

import sys

def Check(a):
  sm=0
  xr=0
  for i in a:
    sm+=ord(i)
    xr^=ord(i)
  if ((sm==0x704)and(xr==0x36)):
    print 'Serial is valid'
  else:
    print 'Serial is not valid'

if __name__=="__main__":
  if len(sys.argv)>1:
    Check(sys.argv[1])
  else:
    print 'Input serial as an argument'

Теперь пишем для него решение:

from z3 import *
let_list=[]
def alphaNumeric(a):
  return Or(And(a>0x29,a<0x3a),And(a>0x40,a<0x5b),And(a>0x60,a<0x7b))

def Check(length):
  i=0
  while i<length:
    globals()['l_{}'.format(i)]=BitVec('l_{}'.format(i),8)
    let_list.append(globals()['l_{}'.format(i)])
    i=i+1
  s=Solver()
  i=0
  while i<length:
    s.add(alphaNumeric(let_list[i]))
    i=i+1
  s.add(reduce(lambda x,y: x^y,let_list)==BitVecVal(0x36,8))
  s.add(reduce(lambda x,y: x+ZeroExt(8,y), [BitVecVal(0,16)]+let_list) == BitVecVal(0x704,16))
  if s.check()==sat:
    return s.model()
  return None

def Find():
  global let_list
  length=2
  while True:
    let_list=[]
    m=Check(length)
    if m!=None:
      break
    length+=1
  print 'Serial: '+reduce(lambda x,y:x+chr(y),['']+[m[i].as_long() for i in let_list])

if __name__=="__main__":
  Find()

Запускаем:

>>> python z3SolveEasyCrackme.py
Serial: mozzWzzygztkhpll
>>> python easycrackme.py mozzWzzygztkhpll
Serial is valid
 

Ломаем настоящий кракми

В качестве практики применим Z3 к настоящему ZeroNights Crackme 2013. Скачать его можно по ссылке.

Запускаем приложение, вводим почту и пароль.

Продолжение доступно только подписчикам

Вариант 1. Оформи подписку на «Хакер», чтобы читать все материалы на сайте

Подписка позволит тебе в течение указанного срока читать ВСЕ платные материалы сайта. Мы принимаем оплату банковскими картами, электронными деньгами и переводами со счетов мобильных операторов. Подробнее о подписке

Вариант 2. Купи один материал

Заинтересовала информация, но нет возможности оплатить подписку? Тогда этот вариант для тебя! Обрати внимание: этот способ покупки доступен только для материалов, опубликованных более двух месяцев назад.


1 комментарий

  1. schoolboy

    23.05.2016 at 16:19

Оставить мнение

Check Also

WTF is APT? Продвинутые атаки, хитрости и методы защиты

Наверняка ты уже читал о масштабных сетевых атаках, от которых пострадали банки, крупные п…