# 答辩补充数据 · 第二批(新实验)· #2 CPU 对等 + #7 符号变量/Z3 超时

> 实验机 `ubuntu@cuda-ke`,git `ee4d03c`。#4(LAVA bug 计数)、#6(覆盖-时间曲线)后台运行中,续报。

---

## #2 · CPU 对等 afl-only 基线(P104/P95 严格归因)

**问题**:现有 afl-only 是**单实例(单核)**基线(`run_afl_only` 仅 `-M fuzzer01`),而 hybrid 用 np=32=32 核——
拿 32 核的 hybrid 比 1 核的 afl-only 不公平,"SymCC 净增"会被追问。

**做法**:libarchive 上跑 **32 个并行 AFL 实例**(1 主 + 31 从,= hybrid np=32 同核预算),300s,量同口径 ShowmapCov。

| 配置(libarchive,300s) | ShowmapCov | 语料 | 备注 |
|---|---|---|---|
| **afl-only(32 并行实例,CPU 对等)** | **27.71%**(3795/13696) | 88,752→抽 17,750 | master FstatsCov 19.61%,execs 9.7M |
| hybrid np=32(F@T30) | 26.95% | — | ~16 AFL + ~16 SymCC |
| ~~afl-only(旧,单核)~~ | ~~更低~~ | — | 不公平,勿用 |

**结论:CPU 对等下,afl-only(27.71%)≈ hybrid(26.95%)——差 0.76pp、在噪声内,SymCC 在 libarchive 上的净贡献 ≈ 0。**
- 这与 **#1**(固定 T=30 消融,增强净增 ≈0)**一致**:把这些核全给 AFL,覆盖不输甚至略好于 hybrid。
- **答辩口径**:承认旧的单核 afl-only 基线不公平;**改用 CPU 对等基线后,libarchive 上 hybrid 不优于 afl-only**。
  (单轮、libarchive 专属;要更硬需多轮多目标。但方向清晰,且与 #1/#5 互证。)
- 数据文件:`exp_showmap/`(afl-only 运行日志)。脚本:`aflonly_cpumatched.sh`。

---

## #7 · 每目标符号变量数 + Z3 超时占比(P55 证据框)

**做法**:给 QSYM 求解器加 `z3_timeout_count_` 计数,并把统计经 **taint 文件**(`SYMCC_TAINT_OUT`)写出
(在 `saveValues` 中写→对 libFuzzer harness 的 `_exit` 也安全,不依赖析构)。各目标跑 5 个种子取均值。

| 目标 | **符号字节 relevant/total**(均值) | 符号占比 | z3_solve | z3_timeout | **超时%** |
|---|---|---|---|---|---|
| gfts-xml | 82 / 96 | 85% | 2089 | 0 | **0%** |
| gfts-png | 41 / 74 | 55% | 268 | 0 | 0% |
| libarchive | 15 / 24 | 63% | 186 | 0 | 0% |
| sqlite | 34 / 183 | 19% | 366 | 0 | 0% |
| pcre2 | 9 / 9 | 100% | 344 | 0 | 0% |
| **freetype2** | **1 / 2183** | **0.05%** | 10 | 0 | 0% |

**读法与结论:**
- **"符号变量数" = relevant_bytes / total**:参与被求解的分支约束的**输入字节数** / 该输入的**总符号字节数**。
  - **freetype2 几乎不符号化**(2183 字节里仅 1 字节进约束)——字体解析绝大多数字节与分支无关,concolic 能撬动的极少;
    这解释了为何 freetype2 上 concolic(纯 MPI)覆盖极低。
  - **xml 高度符号化**(85%)、pcre2 全符号(小输入)、sqlite 中等(19%,SQL 大多是数据不进约束)。
- **Z3 超时占比 = 0%(全部目标,种子输入)**:种子产生的约束都很**易解**(远低于 10s 的 Z3 超时上限)。
  → 说明**求解本身不是瓶颈**(与 D5③/SymSan 评估一致:卡点在 showmap/AFL 集成,不在 Z3)。
  注:fuzz 过程中的对抗性输入可能出现少量超时;此处种子口径给的是**基线**。
- 机制/代码:`solver.cpp` + `solver.h` 加 `z3_timeout_count_` 与 taint 文件首行
  `# relevant total fast_solve z3_solve z3_timeout`(qsym 子模块,重建 `libsymcc-rt.so` 生效,目标二进制热加载不必重编)。
- 数据/脚本:`exp_showmap/sym_stats.py`。

---

## #4 · LAVA-M 注入 bug 计数(afl-only vs hybrid)〔最有说服力〕

**做法**:afl-only 先跑(8 并行 AFL,240s)得语料;hybrid = 在该 AFL 语料上跑 **SymCC 求解**(AFL 探索→SymCC
解 magic 字节),把生成的新输入并入语料;各自 replay 过 cov 二进制数 "Successfully triggered bug N"(listed 集合)。

| 程序 | listed 总数 | **afl-only** | **hybrid(afl+SymCC)** | SymCC 增益 |
|---|---|---|---|---|
| **base64** | 44 | **0 / 44** | **39 / 44**(41 distinct) | **+39** ⭐ |
| uniq | 28 | 0 / 28 | 0 / 28 | 0(见下) |
| md5sum | 57 | 0 / 57 | 0 / 57 | 0(见下) |

**结论(base64,干净有力)**:**AFL 单独 240s 找到 0 个 LAVA bug;加上 SymCC concolic 求解后找到 39/44**——
正是"SymCC 解 AFL 撬不动的 4 字节 magic 守卫"的直接证据。SymCC 在 AFL 的 696 个语料上生成 409 个求解输入,
把 base64 的 39 个 listed bug 全撬开。**这把 deck §5.3 的"应做"变"已做":base64 hybrid 0→39/44。**

**诚实说明(uniq/md5sum)**:这两个上 **SymCC 在其 AFL 语料上生成 0 个新输入**(coreutils 特定:`uniq`/`md5sum -c`
的输入解析符号分支少,单遍 concolic 未产出;且 md5sum 的 AFL 语料仅 1 个——AFL 对 `md5sum -c` 几乎没能扩展),
故 hybrid=afl=0。**base64 是干净的示范目标;uniq/md5sum 需更贴近的种子/更长 concolic 循环(留作补充)。**

参考总注入 bug:base64=44 / md5sum=57 / uniq=28 / who=2136。harness 已独立验证(LAVA 官方 inputs → base64 44/44)。
脚本:`exp_showmap/lava_fix.sh` + `scratch_lava_bugcount.py`。

---

## #6 · 覆盖-时间曲线(300s 是否饱和)

libarchive,8 并行 AFL,3600s,读 `plot_data` 于各时间点:

| t | 120s | **300s** | **900s** | 3600s |
|---|---|---|---|---|
| ShowmapCov | 22.06% | **22.91%** | **28.22%** | 29.54% |
| edges_found | 3020 | 3137 | 3863 | 4044 |

**结论:300s 明显【未饱和】。** 300→900s 覆盖还涨 **+5.3pp**(边 3137→3863,相对 +23%);900→3600s 才放缓到 +1.3pp。
→ **deck 的 300s 数字是【下界】**,再跑到 900s 显著更高。答辩口径:*"300s 未饱和,900s 前仍快速增长;短时窗
低估了可达覆盖"*——这也解释了某些目标 300s 看着一般。数据:`exp_showmap/curve_plot_data`。

---

## 状态(7 项全完成)
| # | 项 | 状态 |
|---|---|---|
| #1 | P147 同超时基线 | ✅ 第一批(Full≈Baseline @T30,两柱等高) |
| #2 | CPU 对等 afl-only | ✅ 27.71% ≈ 26.95%(SymCC 净≈0) |
| #3 | freetype2 逐轮 | ✅ 第一批 |
| #4 | LAVA bug 计数 | ✅ **base64 hybrid 0→39/44**(uniq/md5sum 诚实说明) |
| #5 | 运行配置元数据 | ✅ 第一批 |
| #6 | 覆盖-时间曲线 | ✅ **300s 未饱和**(300→900 +5.3pp) |
| #7 | 符号变量/Z3 超时 | ✅ freetype2 1/2183、Z3 超时 0% |