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

用Python正则脚本自动化提取CTF逆向中的z3约束条件在CTF逆向工程中遇到需要求解大量约束方程的题目时手动提取和整理这些方程既耗时又容易出错。本文将介绍如何编写一个Python正则表达式脚本自动从反汇编代码中提取约束条件并将其转换为z3求解器可直接使用的格式。1. 为什么需要自动化处理约束条件参加过CTF比赛的逆向选手都深有体会当面对几十个甚至上百个约束方程时手动复制粘贴不仅效率低下还容易引入错误。一个典型的场景是反汇编代码中包含大量用或||连接的复杂条件表达式变量命名混乱如v2, v19等需要统一转换为数组索引形式需要处理不等式转等式等特殊情况最终需要将提取的方程整理为z3求解器可接受的格式手动完成这些工作通常需要30分钟以上而使用自动化脚本可以将时间缩短到几秒钟同时避免人为错误。2. 设计正则表达式提取器2.1 核心正则表达式模式我们需要设计一个能够识别以下元素的正则表达式变量名如v2, v19等运算符包括算术和逻辑运算符常量数字比较符号, !, , 等import re # 匹配变量名的模式 var_pattern rv(2[0-9]|1[0-9]|[1-9]) # 匹配整个约束条件的模式 constraint_pattern r([^|])(?:|\|\|)?2.2 变量名转换函数原始代码中的变量名如v2, v19需要转换为数组索引形式v[0], v[1]等。我们可以定义一个转换函数def convert_var(match, shift2): 将v2, v19等变量名转换为v[0], v[17]形式 index int(match.group(1)) - shift return fv[{index}]shift参数用于处理变量编号不从0开始的情况例如第一个变量是v2时shift应设为22.3 不等式转等式处理有些题目会使用不等式条件如v2 ! 100我们需要将其转换为等式def convert_inequality(expr): 将!转换为 return expr.replace(!, )3. 完整预处理脚本实现结合上述组件我们可以构建一个完整的预处理脚本import re def preprocess_constraints(code, shift2): 从反汇编代码中提取并预处理约束条件 参数: 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(rv(2[0-9]|1[0-9]|[1-9]), lambda m: fv[{int(m.group(1))-shift}], expr) # 处理不等式 if ! in expr: expr expr.replace(!, ) processed.append(expr) return processed4. 与z3求解器集成预处理后的约束条件可以直接与z3求解器集成from z3 import * def solve_constraints(constraints, var_count): 使用z3求解约束方程组 参数: constraints: 预处理后的约束条件列表 var_count: 变量总数 返回: 解字典变量名到值的映射 # 创建变量 v [Int(fv{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 None5. 实战案例演示让我们用一个实际例子演示整个流程。假设有以下反汇编代码片段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, shift0)预处理后的约束条件[ 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_count20)得到的解将是一个字典包含各个变量的值{ v0: 78, v5: 125, v7: ..., v12: ..., v13: ..., v15: ..., v16: ..., v17: ..., v18: ..., v19: 83 }5.3 转换为flag最后我们可以将解转换为ASCII字符flag .join([chr(solution[fv{i}]) for i in range(16)]) print(fFlag: {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 性能优化建议当处理大量约束条件时可以考虑以下优化使用z3.Optimize代替z3.Solver进行优化求解对约束条件进行分组并行处理缓存已解析的表达式提示在实际CTF比赛中建议将预处理脚本和求解脚本分开方便调试和复用。7. 完整工具链实现为了最大化效率我们可以构建一个完整的工具链反汇编代码提取工具从二进制文件中提取关键约束代码段约束条件预处理脚本本文介绍的核心功能z3求解器集成自动求解并验证结果结果格式化输出将解转换为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_count16) # 4. 输出flag if solution: flag format_solution(solution) print(fFound flag: {flag}) else: print(No solution found)8. 实际应用中的挑战与解决方案8.1 变量数量不确定有些题目不会明确给出变量数量我们可以从约束条件中提取所有出现的变量计算最大索引值确定变量数量def detect_var_count(constraints): 从约束条件中检测变量数量 max_index 0 for expr in constraints: indices re.findall(rv\[(\d)\], expr) if indices: max_index max(max_index, *map(int, indices)) return max_index 18.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(fv{i})) else: vars.append(BitVec(fv{i}, 32)) return vars8.3 约束条件验证为确保提取的约束条件正确可以添加验证步骤def validate_constraints(original, processed): 验证预处理后的约束条件是否保持原意 # 实现验证逻辑 pass9. 扩展应用场景这种自动化方法不仅适用于CTF逆向还可用于软件漏洞分析中的约束求解程序验证中的路径条件提取游戏破解中的条件绕过算法逆向工程注意请仅在合法授权的场景下使用这些技术。10. 进一步优化方向支持更多语法变体处理不同的反汇编器输出格式智能变量类型推断自动判断使用Int还是BitVec约束简化在求解前简化约束条件交互式调试允许逐步验证约束条件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逆向比赛中约束求解类题目的解题效率将原本需要数十分钟的手工工作缩短到几秒钟同时减少人为错误。掌握这些技巧后你就能更从容地应对复杂的逆向挑战了。