z3Py Манипулирование массивом и экономия времени - PullRequest
Новая
       7

z3Py Манипулирование массивом и экономия времени

0 голосов
/ 26 сентября 2018

Я новичок в z3, и после некоторых исследований я не смог понять, как решить мою проблему.

Исходный код принимает строку в качестве входных данных и создает псевдослучайную строку в качестве выходных данных.Я пытаюсь выяснить, как я могу создать произвольную строку в качестве вывода.

Моя главная проблема заключается в том, что моя программа z3 работает вечно.Это в основном потому, что в исходном коде есть циклы и манипулирующие им массивы.

Мне нужно использовать массив z3, потому что мне нужно использовать BitVec в качестве индекса массива.
Оригинальный код: 

from pwn import *
my_command = ordlist("\x41\x41\x41\x41\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00")

final = ["\x00"]*50
i = 0x0
alpha = []
while i <= 0xff:
    alpha.append(i)
    i = i + 1

v2 = 0
v1 = 0
while v1 < 255:
    v3 = alpha[v1];
    v4 = (v2 + my_command[v1 % 19] + alpha[v1] & 0xFF);
    v2 = v4;
    alpha[v1] = alpha[v4];
    v1 = v1 + 1
    alpha[v4] = (v3 & 0xFF);

v5 = 0
v6 = 0;
v7 = 0;
while v5 < 10:
    v5 = v5 + 1
    v8 = alpha[(v7 + 1)];
    v7 = v7 + 1;
    v9 = alpha[(v8 + v6) & 0xFF];
    v6 = (v8 + v6) & 0xFF;
    alpha[v7] = v9;
    alpha[v6] = v8;
    final[(v5 - 1)] = alpha[((alpha[v7] + v8) & 0xFF)];

Транспонировано в: 

from pwn import *
from z3 import *

solver = Solver()

for i in range(0, 20):
    globals()['b%i' % i] = BitVec('b%i' % i, 32)
    solver.add(globals()['b%i' % i] >= 0x0)
    solver.add(globals()['b%i' % i] <= 0xff)

i = 0x0
alpha = []
while i <= 0xff:
    alpha.append(i)
    i = i + 1

A = Array ('A', BitVecSort(32), BitVecSort(32))
for i in range(0, len(alpha)):
    # A = Store(A,i,alpha[i])
    solver.add(Select(A, i) == alpha[i])

v2 = 0
v1 = 0
while v1 < 255:
    v3 = Select(A, v1)
    v4 = (v2 + globals()['b%i' % (v1 % 19)] + Select(A,v1) & 0xFF)
    v2 = v4
    A = Store(A,v1,Select(A,v4))
    v1 = v1 + 1
    A = Store(A,v4,(v3 & 0xFF))

v5 = 0
v6 = 0
v7 = 0
v8 = 0
v9 = 0

F = [0]*50
while v5 < 10:
    v5 = v5 + 1
    v8 = Select(A,(v7+1))
    v7 = v7 + 1;
    v9 = Select(A, (( v8 + v6) & 0xFF))
    v6 = (v8 + v6) & 0xFF;
    A = Store(A,v7,v9)
    A = Store(A,v6,v8)
    F[(v5 - 1)] = Select(A,((Select(A,v7)) + v8 & 0xFF))

solver.add(F[0] == 0x41)
print solver.check()
print solver.model()

Есть ли способ оптимизировать мой код?
Например, как бы вы перенесли следующий фрагмент кода? 

while v1 < 255:
    v3 = alpha[v1];
    v4 = (v2 + my_command[v1 % 19] + alpha[v1] & 0xFF);
    v2 = v4;
    alpha[v1] = alpha[v4];
    v1 = v1 + 1
    alpha[v4] = (v3 & 0xFF);

Спасибо,Джексон

1 Ответ

0 голосов
/ 29 сентября 2018

В вашей модели нет ничего принципиально неправильного.К сожалению, созданная проблема слишком сложна для z3 (или любого другого решения для SMT).Эти виды алгоритмов перетасовки (хеш или крипто являются основными примерами) точно разработаны, чтобы быть односторонним: легко вычислить, но очень трудно инвертировать.И хотя ваш алгоритм не может быть криптографическим, для z3 все еще слишком сложно разобраться.(В частности, массив становится сильно символически ссылочным, что всегда создает слабое место.)

Одна небольшая точка: я думаю, что все должно быть между 0 и 255;и я вижу, что вы ограничиваете все выходные данные соответственно (& 0xFF) и т. д. Если вся арифметика выполняется по модулю 256, вы можете просто использовать битовые векторы размером 8. Это позволит вам пропустить проверки границ и все маскировки и, кроме того,вызовет проблемы, которые легче решить;хотя я сомневаюсь, что это поможет с этой проблемой.

...