解放双手！写一个通用脚本批量处理CTF逆向中的多元方程组（附Python代码）

解放双手用Python自动化处理CTF逆向中的复杂方程组在CTF逆向工程中遇到需要解多元方程组的情况并不少见。这类题目往往要求选手从反汇编代码中提取数十个甚至上百个约束条件手动处理这些方程不仅耗时耗力还容易出错。本文将介绍如何编写一个通用预处理脚本自动从反汇编代码中提取方程、标准化变量命名、处理逻辑运算符最终生成可直接输入z3求解器的Python代码。1. 理解CTF逆向中的方程组问题典型的CTF逆向题目会要求输入一个字符串通常是flag然后对字符串的每个字符进行一系列数学运算和逻辑判断。反编译后的代码通常会呈现以下特征使用v1到vn这样的变量名表示输入字符串的各个字符大量使用和||连接的条件表达式混合包含等式和不等式变量数量通常在16到32个之间手动处理这类问题时选手需要从反汇编代码中复制所有条件表达式统一变量命名如将v20转换为v[19]处理不等式将!转换为分割逻辑运算符连接的多个方程将最终方程逐个添加到z3求解器中这个过程不仅繁琐而且在处理几十个方程时极易出错。一个小的复制粘贴错误就可能导致无法得到正确解。2. 设计自动化预处理脚本我们的目标是创建一个脚本能够自动完成上述所有预处理步骤。脚本的核心功能应包括变量名标准化将v1-vn转换为v[0]-v[n-1]的数组形式逻辑运算符处理自动识别并分割和||连接的多个方程不等式转换将!转换为以便z3处理方程格式化生成可直接被z3解析的Python表达式2.1 变量名标准化反汇编代码中的变量通常以v加数字的形式命名如v1,v20等。我们需要将其转换为Python列表索引形式v[0],v[19]。import re def standardize_variables(code): # 匹配v后跟1-2位数字的模式 pattern rv(\d{1,2}) # 替换函数将v数字转换为v[数字-1] def replacer(match): num int(match.group(1)) return fv[{num-1}] return re.sub(pattern, replacer, code)2.2 处理逻辑运算符CTF题目中的条件通常用或||连接多个方程。我们需要分割这些运算符得到独立的方程列表。def split_equations(condition): # 替换所有和||为统一的分隔符 normalized condition.replace(, ||).replace(| |, ||) # 分割得到各个方程 equations [eq.strip() for eq in normalized.split(||) if eq.strip()] return equations2.3 不等式转换z3求解器更适合处理等式因此我们需要将不等式转换为等式def convert_inequalities(equations): converted [] for eq in equations: if ! in eq: # 将!替换为 converted.append(eq.replace(!, )) else: converted.append(eq) return converted3. 完整预处理流程结合上述功能我们可以构建一个完整的预处理管道def preprocess_conditions(assembly_code): # 1. 标准化变量名 standardized standardize_variables(assembly_code) # 2. 分割方程 equations split_equations(standardized) # 3. 转换不等式 equations convert_inequalities(equations) # 4. 清理空白和分号 cleaned [eq.replace(;, ).strip() for eq in equations] # 5. 过滤空字符串 return [eq for eq in cleaned if eq]4. 与z3求解器集成预处理后的方程可以直接用于构建z3求解器脚本from z3 import * def solve_equations(equations, var_count): # 创建变量 v [Int(fv{i}) for i in range(var_count)] # 创建求解器 solver Solver() # 添加方程 for eq in equations: # 注意这里使用eval有安全风险仅限在受控环境中使用 solver.add(eval(eq)) # 求解 if solver.check() sat: model solver.model() # 按顺序输出字符 flag .join([chr(model[var].as_long()) for var in v]) return flag else: return No solution found5. 实战案例假设我们有以下反汇编代码片段if ( v1 * 7 546 v2 * 2 166 v3 * 6 v4 v6 * 7 1055 || v2 * 4 v4 v5 * 4 v6 * 7 v8 * 6 v9 v14 * 2 v16 * 8 3107 v5 * 4 336 v2 * 2 v6 * 7 656 )应用我们的预处理脚本assembly_code v1 * 7 546 v2 * 2 166 v3 * 6 v4 v6 * 7 1055 || v2 * 4 v4 v5 * 4 v6 * 7 v8 * 6 v9 v14 * 2 v16 * 8 3107 v5 * 4 336 v2 * 2 v6 * 7 656 equations preprocess_conditions(assembly_code) flag solve_equations(equations, 16) print(Flag:, flag)6. 高级技巧与优化对于更复杂的场景我们可以进一步优化脚本6.1 处理多行条件有时条件会分散在多行需要先合并def merge_multiline_conditions(code): # 移除换行和多余空格 return .join(line.strip() for line in code.splitlines())6.2 自动检测变量数量通过正则表达式找出所有变量名自动确定变量数量def detect_variable_count(equations): variables set() for eq in equations: matches re.findall(rv\[(\d)\], eq) variables.update(int(match) for match in matches) return max(variables) 1 if variables else 06.3 处理特殊运算符有些题目会使用位运算或其他复杂运算符def handle_special_operators(equations): converted [] for eq in equations: eq eq.replace(, _lshift_).replace(, _rshift_) eq eq.replace(, _and_).replace(|, _or_) converted.append(eq) return converted7. 安全注意事项在使用eval执行方程时需格外小心因为恶意构造的方程可能执行任意代码在CTF比赛中通常可以信任题目提供的方程在生产环境中应使用更安全的替代方案更安全的替代方法是构建一个表达式解析器或使用ast.literal_eval等受限评估函数。8. 性能优化建议当处理非常大量的方程时如1000可以考虑以下优化使用z3的批量添加方程接口并行预处理方程缓存已解析的方程使用更高效的字符串处理算法# 批量添加方程示例 solver.add([eval(eq) for eq in equations])9. 错误处理与调试完善的错误处理机制可以帮助快速定位问题def safe_eval_equation(eq, variables): try: # 创建局部命名空间只包含我们的变量 locals_dict {fv[{i}]: var for i, var in enumerate(variables)} return eval(eq, {__builtins__: None}, locals_dict) except Exception as e: print(fError evaluating equation: {eq}) print(fError: {str(e)}) raise10. 扩展应用这套方法不仅适用于CTF逆向还可用于自动化数学题目求解程序分析中的约束求解软件验证中的条件检查密码学题目中的方程求解通过调整预处理规则可以适应各种不同的方程格式和编程语言反汇编输出。11. 完整脚本示例以下是整合所有功能的完整脚本import re from z3 import * class CTFEquationSolver: def __init__(self): self.variables [] def standardize_variables(self, code): pattern rv(\d{1,2}) def replacer(match): num int(match.group(1)) return fv[{num-1}] return re.sub(pattern, replacer, code) def split_equations(self, condition): normalized condition.replace(, ||).replace(| |, ||) return [eq.strip() for eq in normalized.split(||) if eq.strip()] def convert_inequalities(self, equations): return [eq.replace(!, ) for eq in equations] def preprocess(self, assembly_code): # 合并多行 code .join(line.strip() for line in assembly_code.splitlines()) # 标准化变量 standardized self.standardize_variables(code) # 分割方程 equations self.split_equations(standardized) # 转换不等式 equations self.convert_inequalities(equations) # 清理 cleaned [eq.replace(;, ).strip() for eq in equations] return [eq for eq in cleaned if eq] def detect_variable_count(self, equations): variables set() for eq in equations: matches re.findall(rv\[(\d)\], eq) variables.update(int(match) for match in matches) return max(variables) 1 if variables else 0 def solve(self, equations): var_count self.detect_variable_count(equations) if var_count 0: return No variables detected v [Int(fv{i}) for i in range(var_count)] solver Solver() for eq in equations: try: locals_dict {fv[{i}]: var for i, var in enumerate(v)} constraint eval(eq, {__builtins__: None}, locals_dict) solver.add(constraint) except Exception as e: print(fError processing equation: {eq}) raise if solver.check() sat: model solver.model() return .join(chr(model[var].as_long()) for var in v) else: return No solution found # 使用示例 if __name__ __main__: solver CTFEquationSolver() assembly_code v1 * 7 546 v2 * 2 166 v3 * 6 v4 v6 * 7 1055 || v2 * 4 v4 v5 * 4 v6 * 7 v8 * 6 v9 v14 * 2 v16 * 8 3107 v5 * 4 336 v2 * 2 v6 * 7 656 equations solver.preprocess(assembly_code) flag solver.solve(equations) print(Flag:, flag)这套自动化处理流程将原本需要手动处理数十分钟的工作缩短到几秒钟大大提高了CTF逆向题目的解题效率。通过不断优化预处理规则可以应对各种复杂的反汇编代码变体真正实现解放双手的目标。