一页速览
| 代码基线 | fork 自 SymCC（USENIX Security’20），分支 engine-configurable-symsan |
| 主结论（A 级） | 20 轮配对消融，两组均为名义 8 核：当前编排（4 AFL + 3 SymCC）相对旧编排（1 AFL + 6 SymCC），libarchive +0.925 pp、SQLite +2.425 pp；A12 = 0.871 / 0.961，Holm p = 0.00189 / 0.00032。这是本轮唯一等 CPU 的对照。 |
| ⚠ 口径 | Hybrid（8 核）相对 AFL-only（1 核 sanity 基线）+1.305 / +1.290 pp——资源预算不对等，只能作为系统配置参照，不是因果效应 |
| 双引擎 | symcc / symsan 在 6 个真实程序上端到端跑通（3 轮 20 s 均值） |
| 明确不宣称 | 296 项技术各自的独立增益 · 24 h 漏洞数与首次触发时间 · 跨 Magma/FuzzBench 泛化 · 在线闭环净收益 |
全文每个数字都标注来源与等级：A 级 = n=20 独立样本 + bootstrap CI + label permutation + Holm 校正；B 级 = 多轮均值 + 全距；C 级 = 单次或不同 seed 的有界测量（不参与“更优”判断）。
要解决的矛盾
覆盖率制导模糊测试
143,718 execs/s
本项目 png 目标持久模式实测。靠随机变异推进，广度和吞吐都强。
✗ 猜不出精确取值：4 字节魔数命中概率 2⁻³²
动态符号执行（concolic）
1.8 个工作项 / 秒
本项目实测：8 个 worker、180 s、322 个工作项。每项 = 一次完整目标执行 + 符号追踪 + 求解。
✗ 每个用例都要真实执行 + 构造表达式 + 调求解器
混合模糊测试让两者互补。但“怎么让它真的有效”仍是开放问题：ICSE’23 的 CoFuzz 在统一设置下重测 7 个 hybrid fuzzer， 发现三个宣称改进 QSYM 协调模式的工作（DigFuzz / MEUZZ / Pangolin）都没打过 2018 年的 QSYM， 且 hybrid 相对传统 CGF 的边覆盖优势整体有限（原文 “overall limited”）。
两侧数字来自不同目标上的观测，只用于说明量级，不是受控对比。
三个层次的技术挑战
三者层层依赖：语义不保真，求解再快也解错了；求解不可扩展，并行只是把错误放大 N 倍；并行没有有效性设计，再多核也只是重复劳动。
项目进展：十个阶段
推进顺序本身就是一条结论：先解决“能不能并行、能不能交付、能不能观测”，再往上叠算法。 P03 的主要产出是一个负结果（把 CPU 争用当扩展性瓶颈的结论被自己的对照实验推翻并公开修正）；P08 起为当前工作树，尚未提交。
系统构成：五层模块与它们的规模
依赖方向是单向的：benchmark/ 调编译器包装脚本和 mpirun；util/ 通过 ConcolicEngine 契约拼出 argv 与环境去起运行时；
运行时把 telemetry 与候选回传；compiler/ 只负责插 _sym_* 调用，不知道上面几层的存在。这条单向性是双引擎能共存的前提。
构建产物：一份源码，七类二进制
| 变体 | 谁在跑 |
|---|---|
*_symcc | concolic worker |
*_symsan | --engine symsan 的 worker |
*_afl | AFL 实例，以及所有 showmap 判新 |
*_afl_laf / _ctx / _ngram4 / _laf_ctx | 多 profile 并行时的 AFL 从实例 |
*_afl_cmplog | RedQueen 伴随二进制 |
*_native | 基线与崩溃复现 |
一条必须记住的规则：无论哪个引擎产出候选，判新永远用 *_afl 这一个二进制——
这保证 B1/B2 始终在同一个边 ID 空间里，也保证换引擎不会让覆盖率口径漂移。
仓库定义 5 种 AFL 构建变体 × 9 种运行 profile；配置面共 403 个 SYMCC_*，绝大多数默认关闭。
系统架构：七层研究栈
第 ⑦ 层是实现的一部分，而不是实验做完之后补的日志。
最重要的系统不变量：激进提议、保守接纳
解耦了“敢不敢用”和“对不对”：不完备方法可以被大胆引入以提高召回，正确性由独立 validator / replay 守住。学习式与 agentic 模块永远没有授权 UNSAT、覆盖或程序等价的权力。
单个工作项的执行次序
MPI 协议：拉模式 + 内容寻址
三个决策决定了它能不能扩到几十个 worker：拉模式（求解耗时方差极大，推模式下慢 worker 会积压队列）； 传内容对象而非路径（worker 临时目录完全隔离）；只回传稀疏边（候选文件不上行，MPI 流量与 worker 数无关）。
位图与哈希空间：最容易搞错的地方
| 标签 | 生成者 | 哈希空间 | 有最终接纳权？ |
|---|---|---|---|
| B1 master 覆盖图 | AFL 插桩目标 showmap | AFL 边 ID | 是 |
| B2 worker 本地图 | 候选重放的稀疏边 | AFL 边 ID | 否（预过滤） |
| B3 QSYM 分支兴趣图 | 符号分支站点 / 结果 | XXH32(site_id,taken)%65536 | 否 |
| B4 coverage owner 分片 | 多 coordinator 持久状态 | AFL 边 ID | 仅多 master 模式 |
| B5 AFL 数据命名空间 | preload runtime | AFL map 低位保留区 | 注入时与边共同保留 |
| B6 grammar 位图 | parser rule ID | 规则 ID | 否 |
B3 与 B1/B2 是互不相通的 ID 空间。SYMCC_AFL_COVERAGE_MAP 在 worker 中实际指向
131072 字节的 QSYM qsym_bitmap——拿 AFL 边 ID 去索引它得到的分类毫无意义。
再往底一层：本项目 clang-18 走 PCGUARD，guard 下标加载期顺序分配，
__afl_map_size = __afl_final_loc + 1——MAP_SIZE=65536 是起步值而非硬上限。
双引擎抽象：换引擎不换评测口径
两个后端实现原理完全不同（编译期插桩 vs DFSan 标签传播），但共享同一套 triage、调度与冗余统计， 因此两条后端的数字可以放进同一张表比较。
关键技术① 同一段源码，优化器决定 concolic 看到什么
| 形态 | 触发条件 | 约束长什么样 | 求解难度 |
|---|---|---|---|
| A. 宽整数内联比较 | -O2 把 memcmp(a,b,4) 内联成 bswap + icmp | 单个 Equal(Concat(b0..b3), 0x53594D43) | 最容易，可免 SMT |
| B. 存活的 libc 调用 | 长度较大或未内联，命中运行时包装器 | n 个 Equal + n−1 个 And | 中等；没有“部分学分” |
| C. 逐字节循环 | 源码手写循环比较 | N 条独立单字节分支 | 每条都简单，但需 N 次迭代 |
两个实现细节
① -O2 会把 memcmp(...)==0 规范化成 bcmp，
包装器白名单里专门加了它（compiler/Runtime.cpp:226）。漏掉这条会静默丢失整类约束。
② 真实目标构建里从来没有 -fno-builtin——形态 A 是现代主力形态。
fastSolveConcat：连 Z3 都不用
根是关系运算、恰好两个孩子、一侧 ≤64 位常量、另一侧是纯符号输入字节的 Concat 链时， 求解退化成按字节把常量写回输入缓冲区，完全不进 SMT。
边界：不处理 shift-or 拼装或 ZExt(Concat)。
关键技术② 求解代价层次
QSYM 主路径：fastSolve 成功即返回 → 否则先做带完整前缀的严格求解 → 严格 UNSAT/unknown 后，
普通目标退到乐观求解、含 Ite 的进 Backsolver。求解超时是硬编码的
kSolverTimeout = 10000 ms（solver.cpp:52），没有对应环境变量。
关键技术③ 四层过滤漏斗：并行有效性的核心
| 阶段 | 计数 | 占产出 |
|---|---|---|
| concolic 产出 | 3,154 | 100 % |
| → 过 B2（worker 判新） | 299 | 9.5 % |
| → 过 B1（写入语料） | 167 | 5.3 % |
冗余里 34.8 %（1,098 条）是字节完全相同的重复——靠 128-bit BLAKE2b 内容摘要 就挡掉了，连 showmap 重放都省了。这就是第一道闸门必须放在 showmap 前面的原因。
【C 级】xml 目标、8 worker、322 个工作项、180 s 单次实测。
关键技术④ 证明携带的编译期 CFG 变换（IFSS / Hydra）
把多条路径合成一个表达式状态、合并相似控制流臂，从而减少 fork 和重复执行。 错误的变换会直接改变程序语义，因此这一族默认关闭，并使用三层门：
① proof gate
MemorySSA / AA 证明的内存状态合并与 NoMod def-chain。不能证明就 fail closed。
② 未变换基线 replay
以原始 IR 生成的目标作为权威 oracle，只有“变换目标失败而基线没失败”的站点才形成 spurious-failure 证据。
③ denylist
这些站点被永久排除。变换结果绑定 manifest + SHA-256 seal，并在全新 LLVM 进程里独立重放。
覆盖 F248–F296：多臂 region-state worklist、switch 的 linear/balanced/profile-optimal 树、 多出口 exit-id + live-out tuple、affine 自然循环闭式、上三角递推、byte-lane 部分重叠的 continuation 内存。 边界：符合 Hydra 的 failure-preserving 而非完整 semantics-preserving；seal 不等于形式化验证或远程 attestation。
实验方法：证据分级制度
主结论 20 轮配对统计消融【A 级】
主结论的三条读法
① 等 CPU 那一组：编排改动显著有效
+0.925 / +2.425 pp
同为名义 8 核，1 AFL + 6 SymCC → 4 AFL + 3 SymCC。Holm p = 0.00189 / 0.00032，A12 = 0.871 / 0.961。 这是本轮唯一的等 CPU 对照。
② 批次 sanity 未见机器漂移
p = 1.000
两批单实例 AFL-only 之间无差异（均 +0.095 pp），加强了①的可信度。
③ 有信息量，但不是等 CPU 结论
+0.065 → +1.290
同样是 8 核对 1 核，旧编排相对 AFL-only 只有 +0.065 pp（p = 1），当前编排是 +1.290 pp（p = 0.00032）。 同样的不对等下差距如此悬殊，说明多出的 7 个核在旧编排里几乎没换来覆盖率。
同机、同一份当前 SymCC 目标二进制、同批种子、15 s 配置预算、名义 8 核，每组 n=20； 10,000 次 percentile bootstrap + 100,000 次 paired sign-flip randomization + Holm family-wise 校正。
口径提醒：15 s 轮次远小于 AFL 默认跨实例同步周期，主指标是结束后 afl-showmap 对
并集语料的离线边覆盖率，不能解释为“AFL 已利用这些输入继续变异”。
四组配置的 20 轮分布
双引擎六目标基准【B 级】
求解策略的实际构成【C 级】
常见误解是“符号执行都是乐观求解”。默认路径是先严格求解，UNSAT / 超时才退到乐观—— 但保存下来的产出里乐观占 49 %–84 %，说明严格求解在这些目标上 UNSAT 比例相当高。
| 目标 | 种子 | 符号分支 | Z3 严格查询 | nominal | optimistic | optimistic 占比 |
|---|---|---|---|---|---|---|
| lava base64 | 5 B | 70 | 53 | 8 | 41 | 83.7 % |
| libarchive | 6 B | 34 | 22 | 8 | 14 | 63.6 % |
| pcre2 | 11 B | 475 | 133 | 52 | 79 | 60.3 % |
| gfts png | 69 B | 144 | 142 | 51 | 81 | 61.4 % |
| sqlite | 34 B | 63 | 45 | 14 | 31 | 68.9 % |
| gfts xml | 52 B | 240 | 225 | 114 | 111 | 49.3 % |
六个目标上 -backsolve / -poly / -fast 默认配置下产出全部为 0——
SYMCC_BACKSOLVER 虽默认开，但只在分支表达式含 Ite 时触发，这批目标一次都没触发。
因此在这套 benchmark 上，“丢前缀”实际就等于“乐观求解”。
求解技术族消融：完整 Z3 调用下降，但总成本上升【C 级描述】
目前唯一一组把消融粒度下沉到技术族的结果：LAVA-M base64，13 个 public seed × 3 个 profile。
确实起作用的部分
完整路径 Z3 调用 −56.6 %（2,742 → 1,189） 每 seed 候选总数 +33.7 % unique +23.5 %
telemetry 证明技术在跑而非"只配置未运行"：fast_solves 189、backsolver 678/672、poly_cache_entries 2,510、unsat_core_hits 1,333。
但总成本是上升的
① 平均墙钟 0.34 s → 18.25 s（约 53.3 倍）；候选吞吐 465.4 → 11.7 /s（−97.5 %）。
② 完整路径调用虽少，solver queries 反而从 4,303 增到 12,500（+190.5 %），累计 solver time +82.6 %。
③ listed bug 数完全没提升：三个 profile 的均值（21.62/44）与并集（41/44）一模一样。
所以这一节不能用来宣称性能增益。13 个测量单元是不同 seed 而非重复运行、无置信区间， 只能说明机制确实执行及本批实例的数量级——§6.1 第 1 条禁语并未解禁。
三个求解开关到底值不值得开【C 级】
更一般的观察：在这个系统里，“某项技术有没有用”几乎总是“在什么目标形状上有用”。 这正是把开关做成默认关闭、由 profile 与 telemetry 驱动选择的原因。
乐观求解的边际价值取决于输入格式【C 级】
| 目标 | 格式特点 | 策略 | 产出数 | 独有新边 | 边 / 产出 |
|---|---|---|---|---|---|
| gfts xml | 文本，容错 | 严格 | — | 84 | 3.89 |
| 乐观 | — | 97 | 4.12 | ||
| gfts png | 二进制，带 CRC 与魔数 | 严格 | 51 | — | 1.20 |
| 乐观 | 81 | 11（共 41 条新边） | 0.51 |
xml：乐观是主力
文本格式对“前缀被破坏”高度容错——解出来的输入依然是合法 XML 的另一个变体，照样进新代码。
png：副作用真实存在
产出更多（81 vs 51），单产出边贡献却低 2.4 倍。CRC/魔数严格的二进制格式里，破坏前缀往往直接被早期校验拒掉。
重放抖动比想象的大：同一份冻结语料复跑 10 次，xml 严格求解新边在 439–449 之间摆动。 上表只有大小关系稳定，绝对值不要引用。
两条负面结论【C 级】
① 短轮次里不存在在线闭环
两个独立实验（180 s 实跑 + 受控注入）都表明：
· 运行中的 afl-fuzz 不会重扫自己的 queue/，直接丢文件无效；
· 兄弟实例同步要等 10 分钟（-M 默认，-S 为 20 分钟），而轮次是 120–300 s；
· -F foreign_dirs 里从来没有 symcc01/。
⇒ 所有 ≤300 s 的轮次里，concolic 产出一个都没真正进到 AFL 手里。 覆盖率数字是并集口径，本身成立；但不能解释成“AFL 用上了 concolic 的解”。
修复方向明确：AFL_SYNC_TIME=1 + 把 symcc01/ 接进 -F。代码里已有那条路径，只是没接上。
② 多层嵌套下取头 FIFO 的前沿会枯竭
对照实验：fifo 跑了 298 次执行、610 次 Z3 查询（比覆盖率制导多一个数量级），
深度 16 和 32 都只到 10 就停住；无截断的覆盖率制导策略在第 16 代解出深度 16。
⇒ 枯竭的原因是候选队列的截断，不是全局去重——这一点由控制实验直接证伪了早期的错误归因。
种子长度直接决定成败
同一个二进制：8 字节种子第 6 代解出；4 字节种子永远解不出。
因为 n 是 read() 的具体返回值，if (n < 8) 根本不是符号分支——
求解器不能靠翻转循环条件来加长输入。
并行吞吐扩展 ≠ 覆盖率扩展【C 级】
这是理解「为什么要把核让给 AFL」的背景
纯 MPI：吞吐涨约 117×（128 → 15,022 tc/s），边覆盖率只从 5.67 % 挪到 6.26 %。 吞吐与覆盖率明显脱钩——多出来的用例绝大部分落在已覆盖的路径邻域里。
hybrid：用少约 26 倍的用例，拿到更高覆盖率（8.84 % vs 6.26 %）。
⇒ 并行度加速的是「逼近路径邻域上限」的速度，不是上限本身。 想抬高上限，要么换更好的种子，要么把核让给能产生结构性新路径的组件。
gfts-xml，120 s，单轮。大语料 showmap 最多抽样 20,000 文件，覆盖率不能用于精确效率排名； 只有「吞吐涨两个数量级而覆盖率几乎不动」这个量级关系稳定。
与 ICSE’23 统一再评估的关系【论文】
CoFuzz 用 15 个真实程序 × 24 小时 × 5 次重复、Mann-Whitney U 检验，统一重测了 7 个 hybrid fuzzer。 关键公平性处理：hybrid 是“1 核 fuzzing + 1 核 concolic”，所以传统 CGF 一律实现成双实例版本再比。
| 系统 | 原论文声称比 QSYM 高 | 统一设置下实测 |
|---|---|---|
| Intriguer | +12.42 % | QSYM 反高 3.75 % |
| MEUZZ | +6.60 % | QSYM 反高 9.99 % |
| Pangolin | +21.90 % | QSYM 反高 0.17 % |
| 系统 | 原论文声称比 AFL 高 | 统一设置下实测 |
|---|---|---|
| Angora | +27.08 % | +9.01 % |
| Eclipser | +25.15 % | +5.18 % |
这对本项目意味着两件事
① 对照方式必须对齐——Hybrid 要和同 CPU-second 的纯 AFL 比。本轮只完成了两个 名义 8 核 Hybrid 编排之间的公平比较，AFL-only 仍是 1 核 sanity；按 CoFuzz 的做法， 还需要一个 8 核多实例 AFL 对照组。这个缺口明确保留到下一轮。
② 不能只报自己跑赢的那一组——本项目同时给出了旧编排不显著的那两行， 正是因为 CoFuzz 揭示的问题就出在选择性报告上。
2018 年的 QSYM 平均边覆盖最高，15 个程序里 7 个夺冠；DigFuzz / MEUZZ / Pangolin 分别比它低 7.67 % / 5.92 % / 3.51 %。
学术来源与落地边界：借鉴 ≠ 复现
这张表的存在本身就是一项工程纪律：它让“我们实现了 XX 论文”这句话没法含糊说出口。 完整 18 行对照见 Current_Technology_Compendium.md §2.3。
可归纳的五个组合创新
- 多粒度并行的统一闭环——seed、query、schedule、continuation state 四种并行粒度使用版本化、 可互操作的 telemetry / artifact 契约，具体化后汇入同一套 coverage ownership 与可信接纳边界。
- Query IR 作为跨层证据总线——求解复用、字符串、语法补洞、schedule 与 holdout campaign 共享内容身份和验证语义， 使“某个候选是怎么来的、被谁验证过”可以跨层追溯。
- 双覆盖平面——AFL 兼容位图保证生态互操作（解决“能不能用”），显式结构键的 data / grammar / structure 状态 提高调度与研究测量的可解释性（解决“能不能解释”）。
- 激进 proposal、保守 acceptance——本项目最核心的设计取舍，让不完备方法可被大胆引入以提高召回， 正确性由独立 validator / replay 守住。
- 证明携带的系统优化——编译变换、parser forest、solver strategy 和 coverage join 不只输出结果， 还输出可重算的结构证据和 sealed 实验身份，把“实验可复现”从事后补救变成实现的一部分。
工程先进性①
两种原理完全不同的符号执行后端共享同一套评测口径，在开源实现里并不常见。
工程先进性②
bootstrap CI + sign-flip randomization + Holm 校正 + 负对照， 并且给出的是一个会反驳自己的结论：本轮唯一等 CPU 的对照只覆盖两个 Hybrid 编排之间，「混合优于同等算力纯 AFL」并没有得到。
明确不能宣称的四类结论
❌ “全部 296 项技术让覆盖率提高了 X %”——20 轮消融改变的是系统级编排（AFL 实例数 + SymCC worker 数 + AFL profile 同时变），属组合消融，不能拆到单项技术。
❌ “AFL 已在线消费 SymCC 输入并形成闭环”——已被两个独立实验直接证伪。
❌ “漏洞发现速度提高 X 倍”——本轮 160 个测量单元的目标崩溃数均为 0；这只说明本轮没发现崩溃。
❌ “达到 / 超过 SOTA”——缺少统一版本下的等 CPU、多轮、全消融 R 级结果。
| 已知实现边界 | 说明 |
|---|---|
| GenSym / ConDPOR / IFSS / SymCC-str 均为有界实现 | 覆盖论文思想的重要可执行子集，不能用论文名称暗示已复刻全部语义 |
| 学习与 agentic 模块不可信 | 只能排序或提议，不能授权 UNSAT、覆盖或程序等价 |
| proof artifact 有边界 | seal/replay 可检测本地漂移与篡改，不等于形式化验证或远程 attestation |
| LLVM lowering fail closed | 保守拒绝是正确性选择，不是“所有输入程序都已支持” |
| LLVM intrinsic 覆盖不完整 | llvm.umin/smin/umax 仍被 concretize，会在相关数据流处丢失符号表达式 |
已完成 / 进行中 / 待补
下一步
近期（工程）
① 接上 AFL_SYNC_TIME=1 与 symcc01/ → -F，让短预算下的在线闭环真正成立，
然后重新测量在线闭环相对离线并集的净收益——这是当前最大的已知缺口。
② 收尾 300 s 描述性复测与全量回归。
中期（科研证据）
按 research_protocol.py 契约跑一次 sealed confirmatory campaign：
同一工作树快照、相同 CPU-second、随机区组、每格 ≥20 次，并增加 30 min / 2 h / 6 h 或 24 h 的
coverage AUC、首次 bug 时间与 right-censored 生存分析。
这一步做完，当前的 A / B / C 级观察才能升级到 R 级。
中期（能力）
③ 补齐 LLVM intrinsic 语义覆盖（llvm.umin/smin/umax 等）。
④ 把消融粒度从“系统级编排”下沉到技术族级别，至少给出求解复用、portfolio、grammar 三族各自的独立增益。