告别手搓方程！一个Python正则脚本帮你自动提取CTF逆向中的z3约束条件

用Python正则脚本自动化提取CTF逆向中的z3约束条件

在CTF逆向工程中，遇到需要求解大量约束方程的题目时，手动提取和整理这些方程既耗时又容易出错。本文将介绍如何编写一个Python正则表达式脚本，自动从反汇编代码中提取约束条件，并将其转换为z3求解器可直接使用的格式。

1. 为什么需要自动化处理约束条件

参加过CTF比赛的逆向选手都深有体会，当面对几十个甚至上百个约束方程时，手动复制粘贴不仅效率低下，还容易引入错误。一个典型的场景是：

• 反汇编代码中包含大量用&&或||连接的复杂条件表达式
• 变量命名混乱（如v2, v19等），需要统一转换为数组索引形式
• 需要处理不等式转等式等特殊情况
• 最终需要将提取的方程整理为z3求解器可接受的格式

手动完成这些工作通常需要30分钟以上，而使用自动化脚本可以将时间缩短到几秒钟，同时避免人为错误。

2. 设计正则表达式提取器

2.1 核心正则表达式模式

我们需要设计一个能够识别以下元素的正则表达式：

1. 变量名（如v2, v19等）
2. 运算符（包括算术和逻辑运算符）
3. 常量数字
4. 比较符号（==, !=, >, <等）

import re # 匹配变量名的模式 var_pattern = r'v(2[0-9]|1[0-9]|[1-9])' # 匹配整个约束条件的模式 constraint_pattern = r'([^&|]+)(?:&&|\|\|)?'

2.2 变量名转换函数

原始代码中的变量名如v2, v19需要转换为数组索引形式v[0], v[1]等。我们可以定义一个转换函数：

def convert_var(match, shift=2): """将v2, v19等变量名转换为v[0], v[17]形式""" index = int(match.group(1)) - shift return f'v[{index}]'

shift参数用于处理变量编号不从0开始的情况，例如第一个变量是v2时，shift应设为2

2.3 不等式转等式处理

有些题目会使用不等式条件（如v2 != 100），我们需要将其转换为等式：

def convert_inequality(expr): """将!=转换为=="" return expr.replace('!=', '==')

3. 完整预处理脚本实现

结合上述组件，我们可以构建一个完整的预处理脚本：

import re def preprocess_constraints(code, shift=2): """ 从反汇编代码中提取并预处理约束条件 参数: code: 包含约束条件的反汇编代码字符串 shift: 变量编号偏移量（如第一个变量是v2则设为2） 返回: 预处理后的约束条件列表，可直接用于z3求解器 """ # 提取所有约束条件 constraints = re.findall(r'([^&|]+)(?:&&|\|\|)?', code) processed = [] for expr in constraints: # 移除注释和多余空格 expr = re.sub(r'//.*', '', expr).strip() if not expr: continue # 转换变量名 expr = re.sub(r'v(2[0-9]|1[0-9]|[1-9])', lambda m: f'v[{int(m.group(1))-shift}]', expr) # 处理不等式 if '!=' in expr: expr = expr.replace('!=', '==') processed.append(expr) return processed

4. 与z3求解器集成

预处理后的约束条件可以直接与z3求解器集成：

from z3 import * def solve_constraints(constraints, var_count): """ 使用z3求解约束方程组 参数: constraints: 预处理后的约束条件列表 var_count: 变量总数 返回: 解字典（变量名到值的映射） """ # 创建变量 v = [Int(f'v{i}') for i in range(var_count)] # 创建求解器 solver = Solver() # 添加约束条件 for expr in constraints: # 使用eval动态解析表达式 solver.add(eval(expr)) # 求解 if solver.check() == sat: model = solver.model() return {str(var): model[var].as_long() for var in v} else: return None

5. 实战案例演示

让我们用一个实际例子演示整个流程。假设有以下反汇编代码片段：

if ( 7 * flag[0] == 546 && 2 * v19 == 166 && 6 * v18 + v17 + 7 * v15 == 1055 && 2 * v7 + v12 + 7 * v15 + v17 + 4 * v19 + 4 * v16 + 6 * v13 + 8 * v5 == 3107 ) { puts("Success"); }

5.1 预处理阶段

code = """ if ( 7 * flag[0] == 546 && 2 * v19 == 166 && 6 * v18 + v17 + 7 * v15 == 1055 && 2 * v7 + v12 + 7 * v15 + v17 + 4 * v19 + 4 * v16 + 6 * v13 + 8 * v5 == 3107 ) """ constraints = preprocess_constraints(code, shift=0)

预处理后的约束条件：

[ '7 * v[0] == 546', '2 * v[19] == 166', '6 * v[18] + v[17] + 7 * v[15] == 1055', '2 * v[7] + v[12] + 7 * v[15] + v[17] + 4 * v[19] + 4 * v[16] + 6 * v[13] + 8 * v[5] == 3107' ]

5.2 求解阶段

solution = solve_constraints(constraints, var_count=20)

得到的解将是一个字典，包含各个变量的值：

{ 'v0': 78, 'v5': 125, 'v7': ..., 'v12': ..., 'v13': ..., 'v15': ..., 'v16': ..., 'v17': ..., 'v18': ..., 'v19': 83 }

5.3 转换为flag

最后，我们可以将解转换为ASCII字符：

flag = ''.join([chr(solution[f'v{i}']) for i in range(16)]) print(f"Flag: {flag}")

6. 高级技巧与注意事项

6.1 处理特殊变量命名

有些题目可能使用非标准的变量命名方式，如var_1,var_2等。这时需要调整正则表达式：

var_pattern = r'(?:v|var_)(\d+)'

6.2 处理复合条件

对于包含||的复合条件，可能需要保留原始逻辑关系：

def handle_complex_conditions(expr): """处理包含||的复合条件""" if '||' in expr: parts = expr.split('||') return Or(*[parse_constraint(p) for p in parts]) return parse_constraint(expr)

6.3 性能优化建议

当处理大量约束条件时，可以考虑以下优化：

1. 使用z3.Optimize代替z3.Solver进行优化求解
2. 对约束条件进行分组并行处理
3. 缓存已解析的表达式

提示：在实际CTF比赛中，建议将预处理脚本和求解脚本分开，方便调试和复用。

7. 完整工具链实现

为了最大化效率，我们可以构建一个完整的工具链：

1. 反汇编代码提取工具：从二进制文件中提取关键约束代码段
2. 约束条件预处理脚本：本文介绍的核心功能
3. z3求解器集成：自动求解并验证结果
4. 结果格式化输出：将解转换为flag或其他所需格式

def full_pipeline(binary_path): # 1. 反汇编提取约束代码 constraints_code = extract_constraints(binary_path) # 2. 预处理约束条件 constraints = preprocess_constraints(constraints_code) # 3. 求解 solution = solve_constraints(constraints, var_count=16) # 4. 输出flag if solution: flag = format_solution(solution) print(f"Found flag: {flag}") else: print("No solution found")

8. 实际应用中的挑战与解决方案

8.1 变量数量不确定

有些题目不会明确给出变量数量，我们可以：

1. 从约束条件中提取所有出现的变量
2. 计算最大索引值确定变量数量

def detect_var_count(constraints): """从约束条件中检测变量数量""" max_index = 0 for expr in constraints: indices = re.findall(r'v\[(\d+)\]', expr) if indices: max_index = max(max_index, *map(int, indices)) return max_index + 1

8.2 混合类型约束

有些题目可能混合使用整数和位向量，需要特殊处理：

from z3 import BitVec def create_mixed_variables(count, int_vars, bv_vars): """创建混合类型变量""" vars = [] for i in range(count): if i in int_vars: vars.append(Int(f'v{i}')) else: vars.append(BitVec(f'v{i}', 32)) return vars

8.3 约束条件验证

为确保提取的约束条件正确，可以添加验证步骤：

def validate_constraints(original, processed): """验证预处理后的约束条件是否保持原意""" # 实现验证逻辑 pass

9. 扩展应用场景

这种自动化方法不仅适用于CTF逆向，还可用于：

1. 软件漏洞分析中的约束求解
2. 程序验证中的路径条件提取
3. 游戏破解中的条件绕过
4. 算法逆向工程

注意：请仅在合法授权的场景下使用这些技术。

10. 进一步优化方向

1. 支持更多语法变体：处理不同的反汇编器输出格式
2. 智能变量类型推断：自动判断使用Int还是BitVec
3. 约束简化：在求解前简化约束条件
4. 交互式调试：允许逐步验证约束条件

def interactive_debug(constraints): """交互式调试约束条件""" for i, expr in enumerate(constraints, 1): print(f"{i}. {expr}") if input("Keep? (y/n) ").lower() == 'n': constraints.remove(expr) return constraints

这套自动化工具可以显著提高CTF逆向比赛中约束求解类题目的解题效率，将原本需要数十分钟的手工工作缩短到几秒钟，同时减少人为错误。掌握这些技巧后，你就能更从容地应对复杂的逆向挑战了。