побитовые операции с Z3 в python - PullRequest
Новая
       17

побитовые операции с Z3 в python

0 голосов
/ 28 марта 2020

еще раз я борюсь с Z3. Я пытаюсь создать код из двоичного файла, который я разобрал с помощью IDA: ida graph

Эта функция вызывается 0x80 раз. ecx инициализируется с 0x40. [rdi + 8] инициализируется с помощью 0xDEADFACEDEADBEEF. rsi получает каждый байт из вектора "ve c", который я пытаюсь найти, и его значения могут быть только 0x30,0x31 и 0x32. Я не уверен, что мой лог c правильный или я не использую правильную функцию Z3. Это не SAT, и это должно быть, потому что вектор "v1" в моей задаче должен содержать значение 0x123456701234567. Мой код: 

from z3 import *

def set_number(vec,size): #vec
    for i in range(0, size * 8 - 8, 8):
        val = Extract(i + 7, i, vec)
        val = BV2Int(val,False)
        return Or(val==0x30,val == 0x31, val == 0x32)

s = z3.Solver()

size = 0x80
ecx = 0x40
v1 = BitVecVal(0xDEADFACEDEADBEEF,64)
vec = BitVec("inf",size*8) # <content from d.d file>
s.add(set_number(vec,size)) #40 bytes of {0,1,2}

for i in range(0, size*8-8, 8):
    val = Extract(i + 7, i, vec)
    val = BV2Int(val,False)
    if(val == 0x30):
        v1 = RotateLeft(v1, ecx)
        v1 = v1 >> 1
        v1 *= 2
        v1 = RotateRight(v1, ecx)
        ecx = ecx - 1
        s.add(ecx>=0)
    elif(val == 0x31):
        s.add(ecx<40 and ecx>=0)
        ecx = ecx+1
        v1 = RotateLeft(v1,ecx)
        v1 = v1 >> 1
        v1 *= 2
        v1 = RotateRight(v1,ecx)
        ecx = ecx+1
    elif (val==0x32):
        s.add(ecx < 40 and ecx >= 0)
        ecx = ecx + 1
        v1 = RotateLeft(v1, ecx)
        v1 = v1 >> 1
        v1 *= 2
        v1 = v1 | 1
        v1 = RotateRight(v1, ecx)
        ecx = ecx+1
s.add(v1 == 0x123456701234567)
s.check()

Как всегда, большое спасибо!

1 Ответ

2 голосов
/ 28 марта 2020

Здесь есть несколько проблем, но наиболее важной из них является использование if-then-else. Когда вы используете значение symboli c, вы не можете использовать Python if-then-else. Вместо этого вы должны использовать z3's If construct.

В вашей программе ваши if-then-else точно оцениваются, и, таким образом, вы получаете в конце фиктивное утверждение. Вы можете проверить это, поставив print s.sexpr() перед вызовом check.

Начните с замены всех ваших if-then-else's вызовами на функцию If. И на каждом шаге посмотрите на s.sexpr() (скажем, после каждого add) и убедитесь, что он содержит правильные выражения. Это должно привести вас к правильному кодированию проблемы. Начните с чтения здесь: https://z3prover.github.io/api/html/namespacez3py.html#a782883a35d4c6a0be62cd5333645dbaf

Стиль кодирования z3

Ниже описано, как я могу написать вашу проблему в z3py. Обратите внимание, что я просто транслитерировал ваш код python, поэтому, если у вас есть какие-либо ошибки в вашем коде, они будут сохранены. Обратите внимание, что все вычисления Symboli c "if-then-else" выполняются отдельно и объединяются с помощью вызовов If. 

from z3 import *

size = 0x80
vec = BitVec("inf", size * 8)

s = Solver()

# Every byte in vec is either 0x30, 0x31 or 0x32
for i in range(0, size*8, 8):
    b = Extract(i+7, i, vec)
    s.add(Or(b == 0x30, b == 0x31, b == 0x32))

def setLastBit(v):
    return Concat(Extract(63, 1, v), BitVecVal(1, 1))

def clearLastBit(v):
    return Concat(Extract(63, 1, v), BitVecVal(0, 1));

def if30(inp, ecx):
    inp = RotateLeft(inp, ecx)
    inp = clearLastBit(inp)
    inp = RotateRight(inp, ecx)
    ecx = ecx - 1
    return inp, ecx

def if31(inp, ecx):
    ecx = ecx + 1
    inp = RotateLeft(inp, ecx)
    inp = clearLastBit(inp)
    inp = RotateRight(inp, ecx)
    ecx = ecx + 1
    return inp, ecx

def if32(inp, ecx):
    ecx = ecx + 1
    inp = RotateLeft(inp, ecx)
    inp = setLastBit(inp)
    inp = RotateRight(inp, ecx)
    ecx = ecx + 1
    return inp, ecx

v1  = BitVecVal(0xDEADFACEDEADBEEF, 64)
ecx = BitVecVal(0x40, 64)

for i in range(0, size*8, 8):
    val   = Extract(i + 7, i, vec)
    val30 = if30(v1, ecx)
    val31 = if31(v1, ecx)
    val32 = if32(v1, ecx)
    v1    = If(val == 0x30, val30[0], If(val == 0x31, val31[0], val32[0]))
    ecx   = If(val == 0x30, val30[1], If(val == 0x31, val31[1], val32[1]))

s.add(v1 == 0x123456701234567)

print (s.sexpr())
print (s.check())

. Когда я запускаю это, к сожалению, z3 печатает программу, сгенерированную внутри. (Вы можете проверить это, чтобы получить представление о том, как все работает под капотом), но он не возвращается быстро, чтобы сказать sat или unsat. Причин может быть несколько:

  • Алгоритм, который вы закодировали, может быть не совсем правильным. Я бы порекомендовал изучить программу, как я ее написал, и убедиться, что она отражает то, что вы хотели. Посмотрите, можете ли вы следовать сгенерированным программам (вы можете добавить print (s.sexpr()) в Strategi c местах, чтобы увидеть, какой код генерируется на каждом шаге.

  • Если кодировка неверна, тогда надеюсь, вы исправите это в этом стиле, и z3 найдет ваше значение vec. Если оно верное, но z3 не отвечает на ваш запрос в течение разумного промежутка времени, то это просто означает, что проблема слишком сложна для z3 для обработки. Я бы рекомендовал, чтобы ваш vec был коротким: вместо текущего 64-байтового размера, начните с чего-то гораздо меньшего и посмотрите, сможет ли z3 справиться с этим (скажем, несколько байтов для начала.) Это также может включите дальнейшую отладку, если вы правильно поняли алгоритм.

Удачи!

...