文档教程网络安全【免费下载链接】mastgThe OWASP Mobile Application Security Testing Guide (MASTG) is a comprehensive manual for mobile app security testing and reverse engineering. It describes technical processes for verifying the OWASP Mobile Security Weakness Enumeration (MASWE) weaknesses, which are in alignment with the OWASP MASVS.项目地址https://gitcode.com/gh_mirrors/ow/mastg点击查看免费下载本篇技术指南围绕 OWASP Mobile Application Security Testing GuideMASTG知识库中的符号执行Symbolic Execution知识条目展开系统讲解符号执行与混合执行Concolic Execution的核心原理、面临的现实挑战以及如何借助 Angr 等开源二进制分析框架在 Android 移动应用安全测试中落地实践。读完本文你将掌握符号执行的理论模型AST 约束生成、SMT 求解器、路径爆炸并能照搬一个可运行的 Angr 求解脚本自动破解原生层授权/序列号校验逻辑为后续处理混淆过的 native 库提供自动化分析思路。一、从文档定位看符号执行在 MASTG 中的角色本知识条目 MASTG-KNOW-0116 归属于MASVS-RESILIENCE抗逆向工程类别、平台标记为 generic通用。这意味着符号执行不是某个平台的专有技巧而是贯穿 Android、iOS 双平台的通用逆向分析方法。其核心用途体现在求解到达某个代码块所需的输入在逆向中最耗时的任务之一是弄清楚要让程序走到某条成功分支输入应该是什么支撑去混淆de-obfuscation任务例如简化控制流图CFG、逆向基于虚拟机的软件保护VM-based protections与模拟器追踪、动态插桩等手段互补正如 0x04c-Tampering-and-Reverse-Engineering.md 所述在黑客实践中一切皆可用什么最高效就用什么。每个二进制都不同最有效的方式往往是组合手段例如模拟器追踪与符号执行结合。与符号执行强关联的仓库实践包括MASTG-TECH-0037使用 Angr 对 Android License ValidatorMASTG-APP-0002进行符号执行破解的完整 walkthroughMASTG-TOOL-0030Angr 工具条目MASTG-TOOL-0073radare2iOS工具条目MASTG-TOOL-0098iaitoradare2 官方 GUI工具条目。二、符号执行把程序算出来而不是跑出来2.1 核心思想用一阶逻辑公式描述所有可能路径文档指出符号执行在 2000 年代末成为识别安全漏洞的主流测试手段。它的本质是将程序可能经过的路径表示为一阶逻辑公式formulas in first-order logic再用SMTSatisfiability Modulo Theories求解器检查这些公式的可满足性并给出解——包括到达执行路径上某一点所需的变量的具体取值。通俗地说符号执行是在数学层面分析程序而不真正执行它每个未知输入被表示成一个数学变量符号值对这些变量执行的所有操作被记录为一棵操作树即编译理论中的AST抽象语法树AST 被翻译成所谓的约束constraints交给 SMT 求解器解释分析结束时得到一个最终数学方程方程中的变量就是值未知的输入SMT 求解器解出该方程给出在给定最终状态下各输入变量的可能取值。2.2 最小示例(x * y) z文档用了一个精炼的示意假设某函数接收输入x将其乘以第二个输入y随后有一个if条件检查计算结果是否大于外部变量z的值——大于则返回 success否则返回 fail。这个运算对应的方程就是(x * y) z如果我们希望该函数始终返回 success最终状态就可以让 SMT 求解器计算满足该方程的x和y取值。需要注意的是z是外部变量如同全局变量其值可能在本函数之外被改变这会导致每次执行输出不同从而给求解正确解增加额外复杂度。文档也提示SMT 求解器内部使用多种高级方程求解技术这些技术的深入讨论超出了书籍范畴读者只需理解其求解约束、给出可行取值的角色即可。2.3 经典符号执行面临的四大挑战真实世界的函数远比上述示例复杂经典符号执行会遇到挑战成因与后果无限执行树程序中的循环与递归可能导致执行树无限增长路径爆炸path explosion多重条件分支或嵌套条件导致路径数量指数级膨胀方程不可解符号执行生成的复杂方程可能超出 SMT 求解器的求解能力外部交互不可符号化系统调用、库调用、网络事件无法被符号执行处理三、混合执行Concolic Execution符号与具体的融合为了克服路径爆炸典型做法是将符号执行与动态执行具体执行concrete execution结合这一组合被称为concolic execution名称源自concrete symbolic有时也叫动态符号执行dynamic symbolic execution。以上述(x * y) z为例我们可以通过进一步逆向、或动态运行程序先拿到外部变量z的具体值再把这个信息喂给符号执行分析。额外信息能降低方程复杂度、产出更准确的分析结果。配合不断改进的 SMT 求解器与当前硬件速度混合执行可以探索中等规模软件模块约 10 KLOC 量级的路径。去混淆实战佐证文档引用了 Jonathan Salwan 与 Romain Thomas 的工作——他们演示了如何使用动态符号执行混合使用实际执行轨迹、模拟与符号执行逆向基于虚拟机的软件保护即 Triton 框架反 VM 保护的知名研究仓库中以 [#salwan] 标注。这说明在应对 VM 壳、控制流扁平化等混淆手段时符号执行不仅是找输入的工具更是简化控制流图、还原真实逻辑的利器。四、框架选择Angr 与 radare2 等开源生态文档指出即便大多数专业 GUI 反汇编器自带脚本与扩展能力它们仍不适合解决特定类型的问题而逆向工程框架允许你无需依赖重量级 GUI 就能执行并自动化任何逆向任务。多数逆向框架是开源的或免费可用的。支持移动架构的流行框架包括AngrMASTG-TOOL-0030Python 编写的二进制分析框架同时支持静态分析与动态符号concolic分析。给定二进制与目标状态Angr 使用形式化方法静态代码分析技术寻找路径并结合暴力求解到达该状态通常比手工调试、搜索路径快得多。它基于VEX 中间语言内置 ELF/ARM 加载器非常适合处理 native 代码如 Android 原生二进制。自版本 8 起基于 Python 3可通过pip install angr安装*nix、macOS、Windows 均支持。注意Angr 的部分依赖包含 Python 模块 Z3 与 PyVEX 的分支版本会覆盖原版建议使用虚拟环境Virtualenv或官方 Docker 容器隔离。radare2MASTG-TOOL-0073iOS 版条目完整的二进制逆向分析框架配套官方 GUIiaitoMASTG-TOOL-0098提供与 radare2 工作流无缝集成的图形界面适合可视化分析 ELF 二进制。4.1 工具组合的典型分工从 MASTG-TECH-0037 的完整流程可以看出实际工作中的组合套路用iaito / radare2做静态分析定位关键函数、识别输入格式如 Base32、长度约束用Angr做符号执行引擎自动化求解合法输入手工分析如解读 XOR 循环、栈布局为符号执行提供准确的起点/终点地址——这正是混合分析manual symbolic的体现。五、实战用 Angr 求解 Android License Validator 的合法序列号5.1 目标程序与运行方式MASTG-APP-0002Android License Validator是一个在原生代码中实现密钥校验的 crackme打包为独立的 Android ELF 可执行文件。作者 Bernhard Mueller 设计它的初衷即在于原生代码分析比 Java 更困难而真实业务逻辑常以 native 形式存在——混淆代码被放进 native 库正是为了增加去混淆难度因此掌握针对原生二进制的符号执行具有现实意义。该二进制文件位于仓库 Crackmes/Android/License_01/validate可通过 adb 在任意 Android 设备上运行$ adb push validate /data/local/tmp [100%] /data/local/tmp/validate $ adb shell chmod 755 /data/local/tmp/validate $ adb shell /data/local/tmp/validate Usage: ./validate serial $ adb shell /data/local/tmp/validate 12345 Incorrect serial (wrong format).此时我们对合法 license key 一无所知——这正是符号执行登场的情境。5.2 静态分析定位校验逻辑与输入格式在 MASTG-TOOL-0098iaito中打开 ELF。main 函数位于偏移0x00001874注意该二进制是PIE位置无关可执行的iaito 选择以0x0作为镜像基址加载。函数名已被剥离但残留的调试字符串足以提供上下文。逐点记录关键信息偏移0x000018a8调用strlen返回值在0x000018b0与0x10比较 →输入序列号必须是 16 字符随后输入被传给偏移0x00001340的Base32 解码函数→ 16 个 Base32 字符解码后共10 字节原始数据解码结果传给偏移0x00001760的校验函数。上述信息直接告诉我们预期的输入形态接下来深入校验函数0x00001760反汇编见 MASTG-TECH-0037。5.3 读懂校验函数的两个关键点1XOR 解密循环0x00001784起反汇编显示一个循环在0x00001798处执行eor r3, r2, r3XOR 运算循环索引var_14h在0x000017d0与 4 比较、ble 0x1784循环回去——即对输入逐字节进行 XOR 变换。文档在此特意强调XOR 是混淆优先、安全其次场景的常见加密手段不应被用于任何严肃加密频率分析即可破解因此在校验逻辑中一旦出现 XOR 就必须给予特别关注并深入分析。2逐字节比对0x000017dc起XOR 解码得到的值依次与子函数调用0x000016f0、0x0000170c、0x00001728、0x00001744的返回值比较任何一个不匹配bne 0x1854都会跳到 Incorrect serial. 分支0x00001854全部通过则到达0x00001840打印 Product activation passed. Congratulations!。该函数结构并不复杂、可手工分析但在大代码库场景下手工逐条解析既繁琐又耗时——自动化正是符号执行的用武之地。5.4 符号执行求解脚本Angr 引擎可通过对如下路径映射自动确定输入串每个字节的约束从 license 校验的第一条指令0x00001760到打印 Product activation passed 的代码0x00001840。初始化 Angr 需要四步加载二进制到ProjectAngr 中一切分析的起点指定分析起始地址校验函数第一条指令。跳过 Base32 实现可大幅降低求解难度指定目标地址0x00001840成功消息所在代码块指定回避地址0x00001854Incorrect serial 代码块。⚠️地址换算注意事项Angr 加载器会把 PIE 可执行文件加载到基址0x400000因此必须把 iaito 中的偏移加上0x400000再传给 Angr。完整求解脚本如下Angr 9.2.2 验证import angr # Version: 9.2.2 import base64 load_options {} b angr.Project(./validate, load_options load_options) # The key validation function starts at 0x401760, so thats where we create the initial state. # This speeds things up a lot because were bypassing the Base32-encoder. options { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY, angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS, } state b.factory.blank_state(addr0x401760, add_optionsoptions) simgr b.factory.simulation_manager(state) simgr.explore(find0x401840, avoid0x401854) # 0x401840 Product activation passed # 0x401854 Incorrect serial found simgr.found[0] # Get the solution string from *(R11 - 0x20). addr found.memory.load(found.regs.r11 - 0x20, 1, endnessIend_LE) concrete_addr found.solver.eval(addr) solution found.solver.eval(found.memory.load(concrete_addr,10), cast_tobytes) print(base64.b32encode(solution))运行结果示例$ python3 solve.py WARNING | ... | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000. bJACE6ACIARNAAIIA说明由于存在多个合法 license key不同运行可能得到不同解。5.5 深入理解脚本中的关键细节blank_state与add_options从指定地址创建空白初始状态SYMBOL_FILL_UNCONSTRAINED_MEMORY、ZERO_FILL_UNCONSTRAINED_REGISTERS用于处理未约束的内存/寄存器用符号值填充或零填充保证求解器有足够的自由度找到可行解。simulation_manager与exploreAngr 内部在起点与终点之间探索所有路径把对应的数学方程交给求解器返回具体有意义的结果simgr.found列表包含满足搜索条件的所有路径。结果读取与 ARMv7 栈布局脚本用found.memory.load(found.regs.r11 - 0x20, 1, ...)取字符串地址。这并非魔法——反汇编中0x0000176c str r0, [var_20h]表明函数输入指针寄存器 R0被存入局部栈变量var_20h fp-0x20。在 ARMv7 中 R11 即 fp帧指针故R11 - 0x20等价于fp - 0x20正是存放输入指针的位置。endnessIend_LE指定小端序读取Android 设备几乎全部采用小端。符号内存 vs 真实内存脚本读取的是符号内存——字符串及其指针在现实中并不存在但求解器保证给出的解与程序真实执行到该点的结果一致。用found.solver.eval可以这样提问给定当前found状态下这串操作的输出输入addr处必须是什么得到合法序列号后即可回到 Android 设备上运行./validate serial验证。文档结论值得铭记符号执行初学时看似令人生畏需要深入理解与大量练习但相比逐条分析复杂反汇编指令所节省的时间投入是值得的实际工程中通常使用混合技巧——正如上述示例先手工分析反汇编代码、为符号执行引擎提供准确条件再自动化求解。六、延伸在 iOS 平台与更多场景中的应用文档提示更多 Angr 使用示例请参阅 iOS 章节。结合仓库结构符号执行相关能力可继续延伸至MASTG-TECH-0042 / 0044 / 0046 等 iOS 技术条目iOS 平台上类似的符号执行/二进制分析实践MASTG-TECH-0119 等通用技术条目跨平台的逆向技巧体系知识库配套条目 MASTG-KNOW-0116即本文所依据的理论骨架其中还给出了四大挑战的完整列表与 concolic 执行的定义可作为持续查阅的速查卡。从源码结构看MASTG-TECH-0037 末尾的混合分析模式手工定位 符号求解是 MASTG 推荐的通用方法论先静态识别输入格式与关键代码块再用符号执行自动化求解约束最后用动态执行验证结果。这套静态 符号 动态三阶段组合正是应对现实世界中混淆 native 库的高效工作流。赞分享文档教程网络安全【免费下载链接】mastgThe OWASP Mobile Application Security Testing Guide (MASTG) is a comprehensive manual for mobile app security testing and reverse engineering. It describes technical processes for verifying the OWASP Mobile Security Weakness Enumeration (MASWE) weaknesses, which are in alignment with the OWASP MASVS.项目地址https://gitcode.com/gh_mirrors/ow/mastg点击查看免费下载相关推荐OWASP MASTG 实战用符号执行破解 Android License Validator 的原生 ELF 许可证校验OWASP MASTG 实战用符号执行破解 Android License Validator 的原生 ELF 许可证校验 导读 Android Licens文档教程网络安全angr符号执行框架中的常见挑战与解决方案angr符号执行框架中的常见挑战与解决方案 前言 angr作为一款强大的二进制分析框架在符号执行、程序分析等领域有着广泛应用。然而在实际使用过程中开发者经常应用安全开发工具angr用户手册二进制程序静态分析与动态符号执行详解angr用户手册二进制程序静态分析与动态符号执行详解 1. 什么是angr angr是一个功能强大且用户友好的二进制分析平台Binary Analysis应用安全开发工具创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考