时间戳

首页 > 解决方案 > z3Py 数组操作和时间效率

z3 - z3Py 数组操作和时间效率

问题描述

我是 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);

谢谢，杰克逊

标签： z3z3py

解决方案

您的模型实际上没有任何根本性的错误。不幸的是，创建的问题对于 z3（或任何其他 SMT 求解器）来说太难处理了。这些洗牌算法（散列或加密是主要示例）被精确地设计为单向：易于计算但很难反转。虽然您的算法可能不是加密级别的，但对于 z3 来说仍然难以处理。（特别是数组，在符号上被大量引用，这总是会产生一个弱点。）

一个小点：我认为一切都必然在0到255之间；我看到你正在相应地限制所有输出(& 0xFF)等等。如果所有算术都是以 256 为模完成的，你可以简单地使用大小为 8 的位向量。这将允许你跳过边界检查和所有掩码，此外还会产生更容易解决的问题；虽然我怀疑它会帮助解决这个问题。

推荐阅读