jetnoir/metis

# Metis — 漏洞研究流水线 适用于 macOS、Linux 和 Windows 目标的自动化二进制漏洞分类。 流水线阶段：谱调用图筛选 (C2)、具有完整 SSA 内存污点的模板数据流匹配 (C3)、符号污点分析 (C6) 以及设备端动态验证 (C7)。 C1 在 C6 的符号执行循环内部提供硬度感知的路径排名，使用 SAT 骨干分数来推迟相变附近的路径。 ## 流水线阶段 | 阶段 | 文件 | 功能描述 | |-------|------|-------------| | C1 | `exploration_technique.py` | 骨干分数路径优先级排序器（内置于 C6） | | C2 | `c2_rmt.py` | 随机矩阵理论调用图筛选 —— 谱异常检测 | | C3 | `c3_templates.py` | 具有完整 SSA 内存污点的模板数据流匹配 (v2) | | C6 | `c6_taint.py` | 符号污点分析 + 通过 angr + Z3 进行 PoC 合成 | | C7 | `c7_dynamic.py` | 设备端验证：SUBPROCESS / LLDB / DTrace (v2) | ## C1 的作用 当 angr 探索具有多个分支路径的二进制文件时，它通常使用 DFS/BFS，而不会感知每条路径约束的求解难度。 C1 添加了一个 **硬度探针**，通过测量有多少符号输入位被强制（骨干）与自由位来评估每个活跃状态的分数。 - **高骨干** = 大部分输入位被强制 = 刚性约束 = 困难路径 → 推迟 - **低骨干** = 多个自由位 = 灵活约束 = 简单路径 → 优先探索 结果：在混合难度的二进制文件上，**活跃状态峰值减少了 60%**，困难/陷阱路径被自动推迟。 ## 架构 ``` metis/ ├── c2_rmt.py ← C2: C2RMTAnalysis — spectral call graph screen ├── c3_templates.py ← C3: C3TemplateAnalysis — template matching (v2: full SSA) ├── c6_taint.py ← C6: C6TaintTechnique / C6Analysis — symbolic taint ├── c7_dynamic.py ← C7: C7Analysis — dynamic validation (v2) ├── exploration_technique.py ← C1: HardnessExplorationTechnique — backbone path ranking ├── semantic_backbone.py ← Production backbone path: Z3 assumption probing (32ms) ├── dimacs_converter.py ← Legacy: claripy → Z3 bit-blast → DIMACS CNF ├── backbone_probe.py ← Legacy: pysat Glucose3 backbone detection ├── offline_analysis.py ← Full chi-squared analysis pipeline ├── test_pipeline.py ← Unit tests (5/5 passing) ├── benchmark_crackme.py ← Benchmark harness └── crackme_mixed.c ← Test binary with mixed-difficulty paths ``` ## 快速开始 — 完整流水线 ``` import angr, archinfo from metis.c2_rmt import C2RMTAnalysis from metis.c3_templates import C3TemplateAnalysis from metis.c6_taint import C6Analysis from metis.c7_dynamic import C7Analysis, extract_poc_from_c6, C7DeliveryMode from metis.exploration_technique import HardnessExplorationTechnique BINARY = '/usr/sbin/smbd' proj = angr.Project(BINARY, auto_load_libs=False, main_opts={'arch': archinfo.arch_from_id('aarch64')}) # C2 — 结构化筛选 c2_result = C2RMTAnalysis.from_project(proj).run() c2_result.print_report() # z_radius, z_energy, z_entropy # C3 — 排名前 20 的函数上的 template match c3_result = C3TemplateAnalysis(proj).analyse_functions( c2_result.top_function_addrs[:20]) c3_result.print_report() # template hits + confidence # C6 — 针对高置信度 C3 匹配结果的 symbolic taint for addr in c3_result.top_function_addrs[:5]: result = C6Analysis(proj).run( proj.factory.call_state(addr), max_steps=800, extra_techniques=[HardnessExplorationTechnique(threshold=0.75)]) if result.findings: # C7 — on-device validation poc = extract_poc_from_c6(result.findings[0], proj=proj) evidence = C7Analysis(binary=BINARY).validate( poc, mode=C7DeliveryMode.DTRACE, timeout_s=60) evidence.write(f'/tmp/c7_{hex(addr)}') print(evidence.asb_text) # paste into Apple ASB / MSRC / Chrome VRP ``` ## 快速开始 — C1（仅骨干优先级排序器） ``` import angr from metis.exploration_technique import HardnessExplorationTechnique proj = angr.Project('./binary', auto_load_libs=False) state = proj.factory.entry_state() simgr = proj.factory.simgr(state) simgr.use_technique(HardnessExplorationTechnique( threshold=0.75, # defer top 25% hardest (adaptive percentile) probe_timeout_s=0.05, # 50ms budget per state max_score_per_step=16, # cap scoring for large state counts )) simgr.run() ``` ## 独立骨干分析 ``` import claripy from metis.semantic_backbone import semantic_backbone_claripy sym = claripy.BVS('input', 64) constraints = [sym[7:0] == 0x41, sym > 0x4141414141414141] result = semantic_backbone_claripy(constraints) print(f"backbone: {result.backbone_fraction:.2f}") # 0.12 print(f"forced: {result.n_forced}/{result.n_semantic_bits}") print(f"time: {result.probe_time_s*1000:.0f}ms") ``` ## 性能表现 ### C1 骨干探测（语义路径与遗留版本） | 指标 | DIMACS 路径（遗留版本） | 语义路径（当前版本） | |--------|---------------------|------------------------| | `a == 0x42` 骨干 | 0.02 (错误) | 1.00 (正确) | | `x > 0` 骨干 | 0.06 (有噪声) | 0.00 (正确) | | 5×64位，19个约束 | 338 毫秒 | 32 毫秒 | | Tseitin 稀释 | 是 | 无 | ### C1 状态减少 | 二进制文件 | 原版峰值状态数 | 硬度感知峰值状态数 | 提升 | |--------|-------------------|--------------------|-------------| | 线性 crackme | 3 | 3 | — (无路径爆炸) | | 指数爆炸 (2^N) | 256 | 256 | — (均匀难度，正确地无操作) | | **混合难度** | **20** | **8** | **减少 60%** | ### 流水线各阶段耗时 | 阶段 | 典型时间 | 备注 | |-------|-------------|-------| | C2 — 单个 macOS 二进制文件 (~1 MB) | ~30 秒 | CFGFast + 50 次 null 重复 | | C2 — 批量 300 个二进制文件，8 个 worker | ~15 分钟 | `batch_screen.py` | | C3 — 前 20 个函数 | ~60 秒 | 寄存器 + 内存 SSA 污点 | | C6 — 简单函数 | 2–5 分钟 | 紧密的路径约束 | | C6 — 复杂函数 | 10–30 分钟 | 大量分支 | | C7 — DTrace 确认 | 5–15 秒 | Attach + sink 探针 | | C7 — LLDB 崩溃捕获 | 15–60 秒 | LLDB 启动 + 崩溃等待 | ## 理论 基于随机 3-SAT 相变的经验性 P vs NP 研究： - 骨干分数与 CDCL 求解器难度相关（Spearman ρ = +0.43，p = 0.012） - 这是边缘 χ²/nv（变量冻结）的代理指标，而 Survey Propagation 解析计算的就是这一指标 - 这种相关性是特定于计算类的：3-SAT 呈现单调上升，而 3-XORSAT（多项式时间）在阈值前保持平缓 ## 依赖项 ``` pip install angr z3-solver numpy scipy # pysat：仅 legacy backbone_probe.py 路径需要（非生产环境） ``` **C7 运行时依赖项**（无需 pip install —— 均为系统工具）： | 工具 | 模式 | macOS 可用性 | |------|------|--------------------| | `lldb` | LLDB 模式 | 随 Xcode / CLT 附带 | | `dtrace` | DTRACE 模式 | 随 macOS 附带（需要禁用 SIP 或具有授权） | | `subprocess` | SUBPROCESS 模式 | stdlib — 始终可用 | **注意：** 不支持 Python 3.12（angr 兼容性问题）。请使用 Python 3.11 或 3.13。 ## 测试 ``` python3 -m pytest metis/test_pipeline.py -v # 5/5 expected python3 -m metis.benchmark_crackme ```

标签：angr, Conpot, DTrace, LLDB, macOS安全, Maven, PoC合成, SAT求解, Windows安全, Z3求解器, 二进制分析, 云安全监控, 云安全运维, 内存污点, 情报收集, 控制流分析, 漏洞研究, 漏洞验证, 符号执行, 约束求解, 自动化漏洞分类, 路径修剪, 逆向工具, 随机矩阵理论, 静态分析