Решатель уравнений Z3 - операция с битовой маской - PullRequest
Новая
       12

Решатель уравнений Z3 - операция с битовой маской

0 голосов
/ 18 января 2019

После обратного проектирования программы я нашел ограничения.

Я должен найти два числа без знака, таких как: 

x + y = 0xC0ED91BD

и 

x * y = Z

В исходной программе умножение чисел выполняется с помощью инструкции imul.

Z должно быть таким, чтобы при проверке только младших 32 битов Z оно было меньше 60. 

Z & 0x00000000ffffffff < 60

Однако, когда я добавляю второе уравнение в качестве ограничения, z3 дает мне ошибку.

Вот мой код: 

#! /usr/bin/python

from z3 import *
import sys

s = Solver()
result = int(sys.argv[1], 16)

x = Int('x')
y = Int('y')

s.add(x + y == result)
s.add(x > 0, y > 0)
s.add((x * y) & 0x00000000ffffffff < 60)

while s.check() == sat:
    print s.model()
    s.add(Or(x != s.model()[x], y != s.model()[y]))

Обновлен:

Вот код, основанный на рекомендуемом решении: 

#! /usr/bin/python

from z3 import *
import sys

s = Solver()
x = BitVec('x', 32)
y = BitVec('y', 32)

result = BitVecVal(int(sys.argv[1], 16), 32)

s.add(x + y == result)
s.add(x > 0, y > 0)
s.add(x * y < 10)

print s.check()
print s.model()

Двоичный файл является 64-разрядным.

Однако операция умножения выполняется с использованием 32-разрядных целых чисел, как показано ниже: 

mov     edx, [rbp+var_14]
mov     eax, [rbp+var_10]
imul    eax, edx

Так что если eax = 0x425a95e5 и edx = 0x7e92fbd8

Затем, после умножения с использованием инструкции imul, eax будет хранить: 0x00000038.

Оба, биты флага переноса и флага переполнения в регистре EFLAGS будут установлены после него.

1 Ответ

0 голосов
/ 18 января 2019

Проблема здесь в том, что вы объявили x и y как произвольно широкие целые числа, в отличие от битовых векторов фиксированной длины.Просто измените ваши объявления, чтобы они соответствовали тому, какой должен быть базовый размер.Предполагая, что вы хотите, чтобы ваша арифметика выполнялась в 32 бита, вы бы сказали: 

x = BitVec('x', 32)
y = BitVec('y', 32)

.Вы также должны объявить result аналогичным образом: 

result = BitVecVal(int(sys.argv[1], 16), 32)

После внесения этих изменений ваша программа должна нормально работать.

Обратите внимание, что в этом случае маскирование с помощью 0x00000000ffffffff недействительно необходимо;так как числа уже 32-битные.Вам нужно сохранить его, только если ваши x и y больше;скажем, 64 бита.

С учетом вышеуказанных изменений я получаю следующий вывод при запуске вашей программы и вызову ее с 0xC0ED91BD: 

[y = 2123561944, x = 1113232869]
[y = 1440310864, x = 1796483949]
[y = 1171875408, x = 2064919405]
... many other lines ..

Это может показаться запутанным, так как числакажется, больше, чем вы думаете, они должны быть.Но помните, что арифметика над битовыми векторами выполняется по модулю 2^n, где n - размер бита, поэтому результаты на самом деле верны: 

>>> 2123561944 + 1113232869 % 2**32 == 0xC0ED91BD
True
>>> 2123561944 * 1113232869 % 2**32 < 60
True

и т. Д.

...