当前位置：首页 > news >正文

逆向工程中的Z3求解器：以Ciscn长城杯rand0m.pyd为例的加密算法破解

news 2026/3/26 23:42:41

逆向工程中的Z3求解器：以Ciscn长城杯rand0m.pyd为例的加密算法破解

在CTF竞赛和安全研究领域，逆向工程往往需要面对各种复杂的加密算法。当传统分析方法遇到瓶颈时，符号执行工具Z3求解器便展现出其独特价值。本文将以Ciscn长城杯赛题rand0m.pyd为例，深入探讨如何运用Z3求解器破解自定义加密算法，并分享实战中的优化技巧。

1. 逆向工程与符号执行基础

逆向工程的核心在于理解程序行为而不依赖源代码。面对编译后的二进制文件，我们需要通过静态分析和动态调试还原算法逻辑。当遇到加密函数时，传统方法通常包括：

静态反汇编：使用IDA Pro等工具分析控制流
动态调试：通过x64dbg等调试器观察运行时行为
算法还原：识别加密模式与数学运算

然而，当加密逻辑包含非线性运算或复杂约束时，这些方法可能效率低下。此时，Z3求解器的符号执行能力可以显著提升分析效率。

提示：Z3是由微软研究院开发的高性能定理证明器，特别适合求解包含算术、位运算和逻辑约束的方程组。

2. 案例解析：rand0m.pyd加密算法

通过逆向分析rand0m.pyd，我们还原出核心加密函数如下：

def encode(input: int): v0 = input ^ 0x9e3779b9 v0 >>= 0xb v0 = pow(v0, 0x10001) % 0xfffffffd v1 = ((input << 4) & 0xfa3affff) + (input >> 5 >> 0x17) return (v0, v1)

该算法具有以下特点：

非线性变换：包含异或、位移和模幂运算
双输出结构：生成v0和v1两个相关但独立的密文
位操作约束：通过掩码(0xfa3affff)限制数据范围

已知密文对为：

encList = [ 0x12287f38, 0x98d24b3a, 0x4a30f74d, 0xe0f1db77, 0x23a1268, 0xadf38403, 0x88108807, 0xd8499bb6 ]

3. Z3求解器的实战应用

3.1 基础求解模型

初始尝试直接建立方程求解：

from z3 import * s = Solver() x = BitVec('x', 32) v1_enc = ((x << 4) & 0xfa3affff) + (x >> 5 >> 0x17) s.add(v1_enc == encList[i])

然而这种方法往往难以直接获得解，原因在于：

位运算导致方程高度非线性
模运算破坏代数结构
多解情况增加搜索难度

3.2 优化求解策略

通过实践发现以下优化手段效果显著：

策略一：放宽约束条件

s.add(And(encList[i] - 0x10 <= v1_enc, v1_enc <= encList[i] + 0x10))

策略二：增量求解与排重

while s.check() == sat: m = s.model() val = m[x].as_long() if encode(val)[1] == encList[i]: print(hex(val)) break s.add(x != val)

策略三：并行化处理

对不同的密文对启动独立求解进程
利用多核CPU加速计算

4. 完整破解流程与技巧

4.1 破解脚本实现

完整解决方案如下：

import z3 def encode(input: int): v0 = input ^ 0x9e3779b9 v0 >>= 0xb v0 = pow(v0, 0x10001) % 0xfffffffd v1 = ((input << 4) & 0xfa3affff) + (input >> 5 >> 0x17) return (v0, v1) def solve_pair(enc1, enc2): s = z3.Solver() x = z3.BitVec('x', 32) v1_enc = ((x << 4) & 0xfa3affff) + (x >> 5 >> 0x17) s.add(z3.And(enc1 - 0x10 <= v1_enc, v1_enc <= enc1 + 0x10)) while s.check() == z3.sat: m = s.model() val = m[x].as_long() ret = encode(val) if ret[0] == enc2 and ret[1] == enc1: return val s.add(x != val) return None def main(): encList = [...] # 原始密文列表 flag_parts = [] for i in range(0, len(encList), 2): res = solve_pair(encList[i], encList[i+1]) if res is not None: flag_parts.append(f"{res:08x}") print("flag{" + "".join(flag_parts) + "}")