z3Py 数组操作和时间效率答案

【问题标题】：z3Py Array manipulation and time efficiencyz3Py 数组操作和时间效率
【发布时间】：2018-09-26 12:26:38
【问题描述】：

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

谢谢，杰克逊

【问题讨论】：

嗨！欢迎来到 StackOverflow！我建议您根据自己的情况提出一个更具体的问题。另见How do I ask a good question? 和How to create a Minimal, Complete, and Verifiable example。
您至少应该告诉我们您要解决的问题是什么。
我正在尝试找出如何生成特定字符串作为输出。例如，如果输入是“AAAA”，输出将是：“05 6a 75 6e be 6f 56 93 50 23” 我希望控制输出（F[0] == 0x41）

标签： z3 z3py

【解决方案1】：

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

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

【讨论】：