Z3python 异或总和？

小能豆

Z3python 异或总和？

我目前正在尝试用 z3python 解决一些方程，但遇到了无法处理的情况。

我需要BitVecs对某些非 ASCII 字符值进行异或运算，然后将它们相加以检查校验和。以下是示例：

pbInput = [BitVec("{}".format(i), 8) for i in range(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add(Xor(pbInput[0], password[0]) + Xor(pbInput[3], password[3]) == 300)

它导致 z3 类型异常： z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value。

我找到了这篇文章并尝试将一个函数应用于我的password字符串，将以下行添加到我的脚本中： password = Function(password, StringSort(), IntSort(), BitVecSort(8)) 但它当然会失败，因为字符串不是 ASCII 字符串。我不在乎它是否是字符串，我尝试这样做Xor(pbInput[x] ^ 0xff)，但这也不起作用。我找不到有关这种特殊情况的任何文档。

编辑：这是完整的回溯。

Traceback (most recent call last):
  File "solve.py", line 18, in <module>
    (Xor(pbInput[0], password[0]) 
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 1555, in Xor
    a = s.cast(a)
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 1310, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 91, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

如果您知道我该如何进行此操作，我将提前致谢！

阅读 25

2024-12-26

共1个答案

小能豆

您的代码中有两个问题。

Xor仅适用于Bool值；对于位向量只需使用^
使用函数ord将字符转换为整数，然后再传递给xor

您没有提供完整的程序（这总是有帮助的！），但您可以按照以下方式在 z3py 中将该部分编写为完整程序：

from z3 import *

solver = Solver()
KEY_LEN = 10

pbInput = [BitVec("c_{}".format(i), 8) for i in range(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add((pbInput[0] ^ ord(password[0])) + (pbInput[3] ^ ord(password[3])) == 300)

print solver.check()
print solver.model()

这将打印：

sat
[c_3 = 0, c_0 = 97]

（我给了变量更好的名字，以便更正确地区分。）所以，它告诉我们解决方案是：

>>> (0xff ^ 97) + (0x8e ^ 0)
300

这确实是您所要求的。

2024-12-26