# SymCC 并行混合模糊测试 · 工作小结

> 分支 `mpi-parallelism-and-quality`;所有改动均已提交并经端到端实测验证。

围绕在 **SymCC 编译期 concolic 执行**之上构建**多核并行 + AFL++ 混合模糊测试**的目标,
从求解引擎、并行架构、模糊测试集成三条主线做了系统的调研、开发、实验与工程化交付。

---

## 一、调研

围绕「并行符号执行 × 混合模糊测试 × SMT 求解加速」横向评估主流方法,形成**有实测支撑的取舍**:

| 结论 | 方法 | 依据 |
|---|---|---|
| **采纳** | cmplog/RedQueen、AFL++ 持久模式、GRIMOIRE 结构化生成、K-Scheduler 前沿调度、BSFuzz 跨节点分支共享、Fuzzy-Sat 快速求解 | 各有明确增益,见下表 |
| **否决** | laf-intel | cmplog 在嵌套/组合比较上完胜,重复建设 |
| **否决** | 多引擎 ensemble | 天花板仅 +5.8%,投入产出比低 |

并厘清定位:**concolic 的不可替代价值 = 求解 cmplog 也解不了的校验和 / 哈希类约束**。

---

## 二、开发(三条主线)

### ① SymCC 求解引擎(runtime / QSYM 后端)
- **多字节快速求解 `fastSolveConcat`**(创新点):绕过 Z3,直接求解多字节 Concat 的魔数 / 整型比较,
  并首创「重读安全网」在快路径命中后校验,保证 soundness。
- **多分支组求解 `negateGroup`**:一次性翻转连续 / 相邻字段 / 同变量的分支组,含约束集同步 hoist。
- **hash-cons 缓存 1024 → 65536**(可 `SYMCC_EXPR_CACHE_SIZE` 调):消除单条 trace 内热子表达式
  反复重建 → Z3 查询膨胀,是最大的零正确性风险性能收益。
- **污点引导选择性符号化**(`SYMCC_FOCUS_*`)+ **分支密度剖析**(`SYMCC_DENSITY_*`)。

### ② 并行架构(MPI master-worker)
- **拉取式工作窃取** + **自适应 AFL/SymCC 核分配** + **per-worker 策略多样化**。
- **修复 worker 端覆盖率去重**:原实现共享位图从未写入、去重静默空转;改为可增长稠密位图 +
  数据级存在性判定,并做分桶归并。
- **K-Scheduler 前沿调度**(免 CFG 的稀有度代理,`SYMCC_KSCHED` 可选)。
- 自适应主循环轮询、over-split 修复、`iter_unpack`/`heapq.nlargest`、`os.scandir` 导入等多项吞吐优化。

### ③ Fuzzing 集成(AFL++)
- **持久模式 + 共享内存输入**(`__AFL_LOOP` / `libAFLDriver.a`),吞吐大幅提升。
- **修复 cmplog 持久性不匹配**:伴随二进制与主二进制持久性不一致会导致 fork server 握手失败 →
  0% 覆盖;重建持久版 cmplog 以真正启用 RedQueen。持久性检测改用 `##SIG_AFL_PERSISTENT##` 字符串。
- **GRIMOIRE 结构化生成** + 约束提示 token 经 extras 目录注入。

---

## 三、实验与量化

基准覆盖**合成靶**(maze / parser / deep_branches / crypto_check)与**真实靶**
(LAVA-M / libarchive / pcre2 / sqlite / freetype2);并做全项目深度质量审计(3 并行 agent + 自审):
结论一致、无回归。

| 优化 | 实测效果 |
|---|---|
| AFL 持久模式 + 共享内存 | 整体 **5–35×**,典型 png **18×**、xml **7.5×** 吞吐 |
| hybrid 核分配上限 ≈12 worker(其余给 AFL) | sqlite **+18%**,其余无回归 |
| MPI 并行扩展 | np=4 达 **5.7×** |
| ExprCache 1024 → 65536 | Z3 查询显著收敛 |
| laf-intel vs cmplog / ensemble | 量化后否决(依据见调研) |

---

## 四、工程化交付

- **零背景可用**:`README.md`(4 种运行模式 + 环境变量参考 + 排障)、一键 `setup.sh` / `build.sh`、
  `requirements.txt`;新机器 `git clone --recursive && ./setup.sh` 即可。
- **离线分发 `package.sh`**:git-free 打包并自校验。审查中**发现并剔除 227M 无用 vendored 内容**
  (假 `pin.H` 桩下的 Intel PIN 2.14 发行版 200M + 走系统 Z3 时的内置 Z3 源 27M)→
  **文件 6591 → 1177,压缩包 57M → 5.7M**;`--keep-vendored` 可保留。
- 所有改动经**两轮独立 review + 端到端实测跑通**(解压包 → `./setup.sh` → 编译 + 冒烟测试 exit 0)。

---

## 五、难点与创新

- **约束缓存不可靠**:按分支表达式缓存 negatePath 结果依赖路径前缀,不 sound → 定位并规避。
- **`pipefail + grep -q` 的 SIGPIPE 误判**:命中即关管道使上游收 SIGPIPE(141),整条管道被判失败 →
  clang 版本检测假阴性;改为「先捕获再 here-string」修复。
- **持久模式握手一致性**:主 / cmplog 二进制持久性必须匹配,否则 0% 覆盖。
- **多字节无 Z3 求解的 soundness**:以「重读安全网」保证快路径正确。
- **死代码甄别**:假 `pin.H` 配置下大量 pintool 文件为死代码,须区分「在用 / 不在用」再动。
- **嵌套子模块链**(main → runtime → qsym → z3)的完整性与离线打包。

---

## 附:关键提交

| 提交 | 说明 |
|---|---|
| `a4b4842` | AFL 持久模式 + 共享内存(5–35× 吞吐) |
| `25ad3b9` | libarchive/pcre2/sqlite 持久化(可复现脚本) |
| `1b5913c` | 细粒度 concolic 分解(突破 ~12 worker 上限) |
| `840ab65` | 动态工作窃取:自适应粒度 concolic 队列 |
| `01f762a` | 分支密度均衡的工作窃取切分 |
| `0257685` | MPI SymCC/AFL 混合脚本优化与加固 |
| `23ed66b` | 运行时子模块:选择性符号化 + QSYM 更新 |
| `4c2b85a` | SymCC / 并行 / fuzzing 能力 + 质量整体提升 |
| `99c30ba` | 全项目质量审计修复(GRIMOIRE 路径、可复现、热路径、溢出) |
| `e882aa4` | 完整上手文档 + 一键部署脚本 |
| `91c478f` | 文档 / 脚本 review 修复 |
| `f0d64fe` | `package.sh` 离线(免 git)分发 + git-free 构建 |
| `235d7fb` | `package.sh` 支持 .zip |
| `7834860` | 修复 `pipefail + grep -q` 导致的 clang 检测假阴性 |
| `ec5d654` | 默认剔除 227M 无用 vendored(PIN/Z3) |

子模块 HEAD:`runtime f83a729` → `qsym 63d2d5e`(改造后的引擎代码所在)。