时间戳

首页 > 解决方案 > Z3python XOR 和？

python - Z3python XOR 和？

问题描述

我目前正在尝试用 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

如果您对我如何执行此操作有任何想法，请提前致谢！

标签： pythonpython-3.xz3z3py

解决方案

您的代码中有两个问题。

  • 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

这确实是你所要求的。

推荐阅读