使用Z3库逆向解密算法时获取错误明文的问题排查

你的Z3代码虽然得到了SAT结果，但明文不正确，核心原因是没有严格对齐原C代码的密钥生成和复用逻辑，下面详细分析问题并给出修复后的代码：

关键错误点分析 #

1. 密钥生成逻辑完全偏离原代码 #

原C代码中，每个密钥字节是从32位的rand()返回值通过以下公式计算得到的单字节：

v5 = rand(); // v5是32位整数
key_byte = v5 - ((unsigned __int64)((0x7F807F81i64 * v5) >> 39) - (v5 >> 31));

而你的代码错误地把单字节的seed_byte当成了公式中的32位v5，这直接导致密钥计算逻辑完全错误。每个密钥字节都对应一个独立的32位随机数，需要为每个rand值单独定义变量再计算字节。

2. 密钥复用逻辑未还原 #

原代码的31字节密文对应的密钥并非全部独立生成：

• 前16字节：由16个rand()值生成（对应栈上的v9到v13区域）
• 中间8字节：复用前面生成的v10对应的8个密钥字节
• 最后7字节：复用v11（4字节）、v12（2字节）、v13（1字节）对应的密钥字节

你的代码假设所有31个密钥字节都是独立生成的，违背了原代码的内存复用逻辑。

3. 变量粒度设计不合理 #

用248位的单个BitVec表示整个密钥，会导致位提取和计算过程中出现逻辑混乱，应该拆分到单个rand值和明文字节的粒度。

修复后的Z3代码 #

以下代码严格复刻原C代码的逻辑：

from z3 import *

# 目标密文（31字节）
ctext = "9a 60 76 14 8b 36 5a 10 2b 91 c4 6c ab 27 92 99 f8 6a ec 5d 32 20 3d 61 8f c7 fb dd 02 72 bf"
ctext = [int(b, 16) for b in ctext.split(' ')]
assert len(ctext) == 31

s = Solver()

# 原代码生成了16个rand()值，对应密钥的前16字节区域
rand_vals = [BitVec(f"rand_{i}", 32) for i in range(16)]

# 计算每个rand值对应的密钥字节（完全复刻原C公式）
key_bytes = []
for rv in rand_vals:
    mul = rv * 2139127681  # 0x7F807F81的十进制值
    shift_right = LShR(mul, 39)  # 无符号右移39位
    sign_bit = LShR(rv, 31)      # 提取v5的符号位（0或1）
    temp = shift_right - sign_bit
    key_byte = rv - temp
    key_bytes.append(Extract(7, 0, key_byte))  # 取低8位作为密钥字节

# 构建完整的31字节密钥（还原原代码的复用逻辑）
full_key = []
full_key.extend(key_bytes[:16])                  # 前16字节：v9到v13
full_key.extend(key_bytes[1:9])                  # 中间8字节：复用v10的8个字节
full_key.extend(key_bytes[9:13])                 # 后7字节：复用v11的4个字节
full_key.extend(key_bytes[13:15])                # 复用v12的2个字节
full_key.append(key_bytes[15])                   # 复用v13的1个字节

# 定义明文变量，每个字节限制为可打印字符
msg_bytes = [BitVec(f"msg_{i}", 8) for i in range(31)]
for mb in msg_bytes:
    s.add(BV2Int(mb) >= 0x20, BV2Int(mb) <= 0x7E)

# 添加异或约束：密钥字节 ^ 明文字节 = 密文字节
for k, m, c in zip(full_key, msg_bytes, ctext):
    s.add(k ^ m == c)

# 求解并输出结果
if s.check() == sat:
    model = s.model()
    plaintext = ''.join([chr(model[mb].as_long()) for mb in msg_bytes])
    print("解密得到明文：")
    print(plaintext)
else:
    print("未找到可行解")

修复说明 #

1. 对齐密钥生成逻辑：为每个rand()值定义32位变量，严格按照原公式计算密钥字节，包括无符号右移、符号位处理等细节。
2. 还原密钥复用规则：完全按照原代码的内存布局，复用对应的密钥字节，确保异或关系和原代码一致。
3. 细化变量粒度：用独立的8位变量表示每个明文字节，32位变量表示每个rand值，避免位操作混乱。

运行这段代码后，应该能得到原代码中的明文THE SECRET HAS BEEN REMOVED LOL（或匹配密文的正确内容）。

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