使用Z3约束求解器处理哈希操作遇属性错误，如何添加编码与哈希约束？

问题场景 #

目标是求解满足以下Python校验逻辑的字符串x：

import hashlib
from hashlib import md5, sha1, sha256, sha384

flippy = lambda x: bytes.fromhex((m := x.encode().hex())[1::2] + m[::2])
check = lambda x, y: all(
    f(flippy(x)).hexdigest().startswith(g) for f, g in
    zip([md5, sha1, sha256, sha384, sha256], y.split("-"))
)

尝试编写的Z3求解器代码运行时触发错误：

# 假设hash_algorithms是Z3的哈希函数列表，x是Z3符号字符串，y是拆分后的前缀列表
for i, algorithm in enumerate(hash_algorithms):
    solver.add(algorithm(bytes.fromhex((m := x.encode().hex())[1::2] + m[::2])).hexdigest().startswith(y[i:i+5]))
    i += 5

错误信息：

Traceback (most recent call last):
  File "I:\test.py", line 33, in <module>
    solver.add(algorithm(bytes.fromhex((m := name.encode().hex())[1::2] + m[::2])).hexdigest().startswith(secret[i:i+5]))
AttributeError: 'SeqRef' object has no attribute 'encode'

核心问题 #

Z3的符号字符串（SeqRef类型）不是Python原生字符串，无法直接调用encode()、hex()这类Python内置方法。必须使用Z3提供的符号化操作函数来实现字符串、字节序列的转换和处理。

解决方案实现 #

1. 符号化实现flippy逻辑 #

原flippy函数的逻辑是：字符串→编码为字节→转十六进制字符串→交换奇偶位置字符→转回字节。我们需要用Z3 API逐步实现每一步：

辅助函数：字节序列转十六进制字符串（符号化）

from z3 import *

def bytes_to_hex_str(bytes_seq):
    # 对每个字节转换为两位十六进制字符（大写）
    hex_chars = StringVal("0123456789ABCDEF")
    def byte_to_hex(b):
        high = Extract(7, 4, b)
        low = Extract(3, 0, b)
        return Concat(SubString(hex_chars, high, 1), SubString(hex_chars, low, 1))
    # 遍历字节序列，拼接所有十六进制字符
    return Fold(lambda acc, b: Concat(acc, byte_to_hex(b)), StringVal(""), bytes_seq)

辅助函数：十六进制字符串转字节序列（符号化）

def hex_str_to_bytes(hex_str):
    # 确保十六进制字符串长度为偶数
    solver.add(Length(hex_str) % 2 == 0)
    hex_chars = StringVal("0123456789ABCDEF")
    def hex_pair_to_byte(pair):
        high = IndexOf(hex_chars, SubString(pair, 0, 1))
        low = IndexOf(hex_chars, SubString(pair, 1, 1))
        return Concat(ZeroExt(4, high), ZeroExt(4, low))
    # 按两位一组拆分十六进制字符串，转换为字节
    return Fold(lambda acc, i: Concat(acc, hex_pair_to_byte(SubString(hex_str, i*2, 2))), 
               BitVecVal("", 0), 
               Range(0, Length(hex_str)//2))

符号化flippy函数

def symbolic_flippy(x):
    # 字符串转字节序列（对应x.encode()）
    bytes_x = StringToBytes(x)
    # 字节转十六进制字符串（对应hex()）
    hex_str = bytes_to_hex_str(bytes_x)
    # 交换奇偶位置字符：取从索引1开始的步长2的子串 + 从索引0开始的步长2的子串
    len_hex = Length(hex_str)
    swapped_hex = Concat(
        SubString(hex_str, 1, len_hex - 1 if len_hex % 2 == 1 else len_hex),
        SubString(hex_str, 0, len_hex)
    )
    # 十六进制字符串转回字节（对应bytes.fromhex()）
    return hex_str_to_bytes(swapped_hex)

2. 添加哈希前缀约束 #

Z3内置了MD5、SHA1、SHA256、SHA384等哈希函数，输入为字节序列，输出为对应长度的位向量。需要将哈希结果转换为十六进制字符串，再检查是否以指定前缀开头：

# 初始化求解器
solver = Solver()

# 定义符号变量：x是待求解的字符串
x = String('x')

# 假设y是已知的校验字符串，例如"ABCDE-FGHIJ-KLMNO-PQRST-UVWXY"
y = "ABCDE-FGHIJ-KLMNO-PQRST-UVWXY"
prefixes = y.split("-")

# 哈希算法映射：Z3函数对应原Python的hashlib函数
hash_funcs = [MD5, SHA1, SHA256, SHA384, SHA256]

# 生成flippy后的符号字节序列
flipped_bytes = symbolic_flippy(x)

# 遍历每个哈希算法和前缀，添加约束
for func, prefix in zip(hash_funcs, prefixes):
    # 计算哈希值（位向量）
    hash_result = func(flipped_bytes)
    # 将位向量转换为十六进制字符串
    hash_hex = bytes_to_hex_str(hash_result)
    # 约束哈希十六进制字符串以指定前缀开头（统一转为大写匹配）
    solver.add(PrefixOf(StringVal(prefix.upper()), hash_hex))

# 求解并输出结果
if solver.check() == sat:
    model = solver.model()
    print("找到解：", model[x])
else:
    print("无解")

关键说明 #

• Z3的符号变量操作必须使用Z3原生API，不能混用Python原生字符串方法
• 字节与十六进制字符串的转换需要手动实现符号化逻辑，因为Z3没有直接对应的内置函数
• 哈希结果是位向量类型，需要转换为十六进制字符串后再进行前缀匹配

内容的提问来源于stack exchange，提问作者MegaMagnum