将 z3 BitVec 转换为字节

Question

如何在检查可满足性之前将密钥转换为字节并将其传递给 sha256。

注意脚本比这个大，但我的问题在这里：

from hashlib import sha256
from z3 import *

key = BitVec('k', 8)
# key = [BitVec(f'key_{i}', 8) for i in range(6)]

h = sha256(key).digest()
print(h.hex())

我不想首先检查可满足性，因为约束必须在密钥生成中呈现。

Answer 1

你不能。由

sha256

实现的

hashlib

不是一种可以处理符号键值的算法。如果您希望它能够处理符号值，您必须编写自己的版本来知道如何处理 z3 的符号值。

根据您正在编码的算法，这可能是一项相当困难的任务。要了解如何使用符号值进行编程，您可以首先阅读 https://theory.stanford.edu/~nikolaj/programmingz3.html

我应该补充一点，如果你的目标是找到产生某个具体输出值的“输入”，那么你会感到失望。没有任何 SMT 求解器可以“逆向工程”像 SHA256 这样的算法，SHA256 是一种设计为单向函数的算法。 （如果你的输入真的很小，你可以解决这个问题；本质上是通过枚举；但对于任何合理的输入大小，这个问题实际上是棘手的。）