Использование Python Z3 с QWORD - PullRequest
Новая
       11

Использование Python Z3 с QWORD

0 голосов
/ 03 декабря 2018

Я новичок в z3py.

Я занимаюсь обратным проектированием кода, в котором у меня есть два QWORD, хранящихся в регистрах XMM.

И с ним выполняются различные операции.

Допустим, мне нужно найти 2 qwords, p1 и p2, учитывая следующие уравнения: 

x = p1 + p2
y = p1 ^ p2

if x == r1 and y == r2:
    print p1, p2

Примечание: P1 и P2 - это QWORD, которые фактически представляют 8-символьную строку ASCII.Итак, P1 - это массив из 8 байтов, где каждый байт соответствует значению ASCII печатного символа.

Я написал следующий код: 

#! /usr/bin/python

from z3 import *

s = Solver()

a = BitVec('a', 64)
b = BitVec('b', 64)

s.add(a + b == result1)
s.add(a ^ b == result2)

if s.check():
    print(s.model())

Вопрос:

Я думаю, что в моем случае не следует использовать BitVec для представления QWORD, поскольку я знаю, что каждый байт QWORD соответствует печатному символу ASCII.Итак, как мне представить мои данные?

1 Ответ

0 голосов
/ 03 декабря 2018

Возможно, вместо этого лучше использовать массив Python из 4-х 8-битных значений: 

#! /usr/bin/python

from z3 import *

s = Solver()

A = [BitVec('a%s' % i, 8) for i in range(4)]
B = [BitVec('b%s' % i, 8) for i in range(4)]

s.add(A[0] <= 128)
s.add(A[0] + B[0] == 12)
s.add(A[1] + B[1] == 5)
s.add(A[2] ^ B[2] == 9)
s.add(A[3] >= 20)

if s.check() == sat:
    print(s.model())

Это печатает: 

[a2 = 0,
 b2 = 9,
 a3 = 20,
 b1 = 0,
 a1 = 5,
 b0 = 140,
 a0 = 128]

Таким образом, вы можете добавить произвольные ограничения, используяэлементы массива естественным образом.

...