# 并行符号执行框架近期工作与下一步科研计划

## 摘要

本项目围绕“利用并行符号执行提升 fuzzing 覆盖率”这一目标，对 SymCC/QSYM
式编译型 concolic execution 进行了系统性重构。近期工作不再把符号执行视为
单次路径翻转器，而是把它提升为一个跨编译器、运行时、求解器、AFL 覆盖反馈、
MPI 分布式调度和 agentic 路由的混合执行框架。

核心思想是：将符号执行中的路径、约束、输入结构、目标分支、worker 状态和
覆盖收益统一建模为可学习、可恢复、可分片的执行任务。这样可以减少并行
concolic execution 的重复求解，提升对结构化输入和隐式信息流的覆盖能力，并
为后续科研实验提供可消融、可复现的工程基础。

本阶段已完成从“并行运行多个 SymCC 实例”到“上下文感知的并行混合符号执行
系统”的关键跃迁。下一步工作将集中在三个研究问题上：

1. 如何让 concolic execution 在大规模并行下保持接近线性的有效覆盖收益。
2. 如何把路径树、结构化输入、solver-hostile 约束和 LLM/agentic 推理结合起来。
3. 如何用严格实验、消融和统计检验验证这些优化确实优于现有 SOTA 组合。

## 一、研究定位

项目定位是开发通用并行符号执行框架，并以 fuzzing 覆盖率提升作为主要评价指标。
相关论文常发表于 Security、Software Engineering、Systems 等会议，但本项目的
核心任务是测试生成、路径探索和覆盖优化，不涉及攻击链、利用生成或漏洞武器化。

当前系统的研究对象包括：

- 编译型 concolic instrumentation 的表达能力和低开销传播；
- SMT、polyhedral abstraction、近似求解和反向路径适配的组合；
- AFL bitmap、data coverage、comparison taint 和路径 DAG 的统一反馈；
- MPI 多 worker 下的 seed-worker-state 联合调度；
- 面向结构化输入的 agentic/LLM 路由和验证式回灌。

## 二、近期已完成工作

### 1. Backsolver + Veritesting：从常量 PHI 到 bounded easy-region 合并

近期对 compiler instrumentation 做了关键扩展。此前 Backsolver 只依赖 LLVM
`select` 和少量常量 PHI 生成 ITE 表达式，覆盖范围有限。现在编译器可以识别
canonical two-arm diamond，并将 PHI incoming 值恢复为 ITE：

- incoming 值可以是常量；
- 可以是 merge 点可见的符号 SSA 值；
- 可以是分支内部的 bounded side-effect-free SSA 表达式；
- 支持整数/浮点/指针标量上的算术、比较、cast、select；
- 对 load、store、call、division、remainder、loop 和非规范 CFG 保守回退。

这使 Backsolver 不只处理“常量分类标签”这类隐式流，也能处理分支内部计算后再
merge 的实际程序模式。运行时侧继续使用已有的 ITE controller 枚举、直接候选
验证和 Z3 fallback，保证输出仍经过 concrete replay/表达式求值验证。

相关测试：

- `test/backsolver_symbolic_phi.ll`
- `test/backsolver_veritesting_region.ll`
- `test/backsolver_implicit_flow.ll`
- `test/backsolver_selective_prefix.ll`

科研意义：

- 这是 Backsolver 思想在编译型 concolic 框架中的轻量化实现；
- 它引入了 Veritesting 的静态合并精神，但避免全 CFG 静态符号执行的复杂度；
- 后续可以继续扩展到 loop template、multi-exit region 和 control-dependence IR。

### 2. S2F 式 dual executor 与 actionseed

系统已加入 S2F 风格 actionseed 机制。MPI coordinator 从 prefix DAG 中选择同一
seed 下的多个高价值 open branch，并生成动作文件：

- `solve`：强制精确求解该目标；
- `sample`：使用 sampling executor profile；
- `skip`：记录但跳过低价值分支。

QSYM runtime 读取 `SYMCC_S2F_ACTIONS`，在目标分支 prefix 达到时绕过普通 pruning。
这让符号执行不再只在当前执行路径上“看到一个分支、翻转一个分支”，而是可以由
coordinator 显式注入同一 seed 的多分支计划。

科研意义：

- 将求解策略从 runtime 局部启发式上移到全局 prefix DAG；
- 为 TACO-Fuzz 的 extended path conditions 和 ConcoLLMic 式 agentic route 提供执行载体；
- 允许对 exact/tailored/sampling executor 做细粒度消融。

### 3. TACO-Fuzz + MultiGo：目标中心路径选择与多路径难度建模

`PrefixDAG` 已加入 target-centric 和 multi-path directed hybrid fuzzing 逻辑：

- 维护 site frequency 与 Poisson-style path difficulty；
- 为 target path 记录 visits、reward、distance、under-exploration；
- 在 replay/actionseed 选择中融合 target distance、path difficulty、mutation rarity；
- 对高价值同 seed 分支批量生成 actionseed；
- 将 under-explored target path 作为 seed selection/generation 的核心信号。

科研意义：

- 传统 directed fuzzing 往往只看静态距离，容易反复挖同一条近但不可达路径；
- 当前实现把“路径难度”和“目标路径多样性”显式加入调度；
- 后续可以研究基于 causal bandit 的目标路径因果收益估计。

### 4. Pangolin 式上下文复用与 sampling 求解

运行时已经提供 prefix-sensitive polyhedral/Z3 context reuse：

- 约束上下文按 prefix key 缓存；
- 保存 SAT/UNSAT/model/linear context；
- 支持 polyhedral byte-box sampling、template pair 和 John-walk 风格采样；
- 与 S2F sampling action、AFL hint mutator 和 coordinator telemetry 打通。

科研意义：

- 把符号执行从“一次 query 一个 model”推进到“一个可复用 path context 产生多个候选”；
- 减少多 worker 对相似 prefix 的重复 Z3 调用；
- 为 solver portfolio 学习提供可观测的 cache hit/sample yield。

### 5. AFL 原生 data coverage map 与 comparison taint

编译器/runtime/coordinator 已支持 AFL 原生 data coverage：

- 记录常量比较的 matched prefix bits；
- 记录 comparison taint locality；
- 通过 AFL bitmap feature 和 coordinator dominance policy 进行筛选；
- 生成 `.compact_focus_set`，作为 Gordian-style compact input linearization 的输入。

科研意义：

- code coverage 不足以描述“距离解析成功还差多少字节”；
- data coverage 能提供连续信号，帮助 fuzzer 和 concolic executor 选择更有潜力的 seed；
- comparison taint 是 Cottontail 式结构化路径表示的低成本近似。

### 6. UCSan 式 under-constrained execution

系统已实现 opt-in 的 compilation-based under-constrained execution：

- 支持函数入口 harness 生成；
- structured seed import/export；
- pseudo/shadow pointer metadata；
- lazy JIT object provisioning；
- pointer load/store/memcpy shadow propagation；
- external policy 与 wrapper 配置。

科研意义：

- 允许符号执行从完整程序 fuzzing 进入函数级、对象图级测试；
- 可以弥补 fuzzing 对深层库函数入口到达困难的问题；
- 后续可与 LLM/object-seed synthesis 结合，生成结构化对象初始状态。

### 7. GenSym 式 state-level parallelism

新增 `StateShardCoordinator`，把一个 work item 抽象为 continuation-like state：

```text
state = input_digest/path + focus_slice + target_branch + s2f_actionseed
```

该 state 被 hash 到 `SYMCC_STATE_TASK_SHARDS`，并映射到 owner worker。MPI master
派发时优先选择 worker 本地 shard，必要时允许 bounded work stealing。状态任务的
lease、completion、reward 和 failure 会持久化到 `.state_tasks.json`。

科研意义：

- 这是 GenSym “branching as concurrency/continuations”思想在现有 SymCC/MPI 架构
  中的工程化折中；
- 不需要重写整个 symbolic execution compiler，即可获得 continuation-level scheduling；
- 后续可扩展为多 coordinator、多 coverage owner 的分布式符号执行控制面。

### 8. Cottontail / ConcoLLMic / Gordian 式 agentic route

`agentic_concolic_hooks.py` 已从简单 hint 加载扩展为 route-aware planner：

- `cottontail` route：从 comparison taint 学习结构局部 focus slice；
- `concollmic` route：把 target branch 映射为 actionseed solve；
- `gordian` route：把 solver-hostile 的 timeout/unknown/no-output 任务送入 sampling route；
- `hybrid` route：三者同时启用；
- 外部 hints 可覆盖 `focus_bytes`、`focus_set`、`target_branch`、`strategy`、`s2f_actions`、`route`。

默认内置 planner 是确定性的，不主动调用模型；外部 LLM/agent 可以通过
`SYMCC_AGENTIC_OUT`、`SYMCC_AGENTIC_HINTS`、`SYMCC_AGENTIC_CMD` 参与调度。

科研意义：

- 避免把 LLM 放进不可控的 trusted execution loop；
- 让 LLM 作为“可验证候选生成器/调度建议器”，输出仍由 concrete replay 与 coverage triage 验证；
- 为比较 Cottontail、ConcoLLMic、Gordian 风格方法提供同一工程接口。

## 三、当前创新点

### 创新点 1：跨层统一的路径上下文反馈

系统把路径 prefix、solver telemetry、AFL bitmap、data coverage、comparison taint、
target branch、worker 状态和 actionseed 统一进 coordinator 的决策模型。这区别于
传统 hybrid fuzzing 中“fuzzer 管 corpus，symbolic executor 管约束”的松耦合结构。

### 创新点 2：Backsolver 与 Veritesting 的编译型轻量融合

不是实现一个完整静态 symbolic executor，而是在 SymCC instrumentation 阶段恢复
控制依赖值为 ITE，并交给运行时 Backsolver 验证。这是一条工程复杂度较低、适合
现有编译型 concolic 框架的路径。

### 创新点 3：continuation state 分片，而不是 seed 文件分片

并行符号执行的重复主要来自“不同 seed 触发相似 symbolic state”。因此调度单位
从文件提升为：

```text
input + focus + target + action plan
```

这比普通 seed queue 更接近符号执行真实的任务边界，也更适合 work stealing 和恢复。

### 创新点 4：LLM route 与 SMT/replay 的可验证组合

系统不让 LLM 直接决定结果正确性。LLM 或内置 agent 只能改变 route、focus、strategy
和 actionseed，最终候选必须由 target execution、telemetry 和 AFL coverage triage
验证。这为 LLM-assisted symbolic execution 提供了可复现、可消融的实验边界。

## 四、主要技术挑战

### 挑战 1：并行 concolic execution 的结构性冗余

多 worker 并发时，即便输入不同，也可能反复翻转相同下游 branch，产生高度重复的
候选。简单增加 worker 数通常会导致有效覆盖收益快速饱和。

当前缓解手段：

- seed-worker contextual bandit；
- state shard owner-local dispatch；
- prefix DAG replay cooldown；
- bitmap/data feature dominance；
- S2F actionseed 让同一 seed 的多个分支计划化。

后续挑战是证明这些机制在真实 benchmark 上能提高 CPU-hour normalized coverage。

### 挑战 2：静态 region merging 的 soundness 与覆盖范围

当前 Veritesting easy-region 只复制 side-effect-free SSA。扩展到复杂 CFG、loop、
memory read 和 external call 会带来 dominance、UB、alias 和路径条件组合问题。

后续需要：

- 明确 region admissibility 判定；
- 建立 instrumentation soundness 约束；
- 引入 loop template 或 bounded unrolling；
- 对每类 IR pattern 增加 lit + differential replay 测试。

### 挑战 3：LLM/agentic route 的可控性

LLM 可以产生结构化输入，但也可能生成无效、不可复现或污染实验的数据。

当前约束：

- 默认 deterministic planner；
- 外部 hint 只影响调度，不直接接受输出；
- 所有候选仍走 concrete execution 和 coverage triage；
- route policy 可用 `SYMCC_AGENTIC_ROUTE` 消融。

后续需要在实验中区分“LLM 语义收益”和“额外 mutation budget 收益”。

### 挑战 4：评价指标的学术严格性

仅报告 generated count 或单次 coverage 曲线不够。需要 equal CPU budget、重复实验、
置信区间、消融和统计检验。

建议采用：

- edge coverage / branch coverage / data feature coverage；
- time-to-first-target；
- unique useful testcases per CPU-hour；
- solver time、Z3 timeout、cache hit、backsolver sat；
- worker redundancy、state shard steal rate；
- Mann-Whitney U 或 bootstrap confidence interval。

## 五、下一步科研计划

### P0：实验严谨化与论文级评估

目标：把当前工程成果转化为可投稿/可复现实验结果。

任务：

1. 建立 benchmark matrix：
   - text parser：json、xml、pcre2、sqlite；
   - binary parser：libpng、libjpeg、woff/font；
   - compression/archive：zlib、libarchive；
   - coreutils-style utility programs；
   - synthetic microbenchmarks for implicit flow、state sharding、data coverage。
2. 设计消融组：
   - baseline SymCC + AFL；
   - + telemetry scheduler；
   - + Pangolin poly cache；
   - + Backsolver/Veritesting；
   - + S2F actionseed；
   - + TACO/MultiGo；
   - + state shard coordinator；
   - + agentic route。
3. 固定 equal CPU budget：
   - 1、4、8、16、32 workers；
   - 30min、2h、6h 三档；
   - 每组至少 20 次随机重复。
4. 输出统计报告：
   - coverage curve；
   - AUC；
   - final coverage；
   - confidence interval；
   - solver cost breakdown；
   - worker redundancy heatmap。

预期论文贡献：

- 一个完整的 parallel hybrid symbolic execution 框架；
- 一组可复现的跨层消融结果；
- 对并行 concolic 冗余瓶颈的实证分析。

### P0：完整 ESCT/ECT 路径结构表示

目标：从当前 branch_trace/data_taint telemetry 推进到 Cottontail 式 expressive
coverage tree。

任务：

1. 将 branch trace、comparison taint、data features、call/ret site、basic block
   事件统一成路径树；
2. 为每个节点记录：
   - path condition summary；
   - input byte dependency；
   - parser locality；
   - target distance；
   - solver outcome；
   - generated candidate quality。
3. 输出 JSON schema，供 LLM/agentic route、offline analysis 和 benchmark 复用；
4. 在 coordinator 中用 ESCT 节点替代部分 flat branch list。

技术挑战：

- 控制路径树规模；
- 对 loop 和 repeated parser states 做压缩；
- 保持 telemetry 输出低开销；
- 让 schema 对 SymCC/SymSan/未来 backend 通用。

### P0：state shard coordinator 的多 master 扩展

目标：从单 master 多 worker 扩展到多 coordinator 协同。

任务：

1. 将 `.state_tasks.json` 拆为 append-only shard logs；
2. 将 AFL bitmap delta journal 扩展为 coverage-owner shard；
3. 设计 coordinator 间 gossip/merge 协议；
4. 引入 lease fencing，避免两个 master 同时派发同一 continuation state；
5. 测试非共享文件系统下的 CAS object transport。

科研问题：

- 多 coordinator 下 coverage novelty 如何去重；
- state ownership 与 worker locality 如何平衡；
- gossip 延迟对 useful coverage 的影响。

### P1：Backsolver/Veritesting 的语义扩展

目标：从 canonical diamond 扩展到更一般的 IFSS/easy-region。

任务：

1. 增加 bounded multi-block region discovery；
2. 对 acyclic CFG 做 post-dominator merge 识别；
3. 支持 select/PHI 链式 ITE folding；
4. 引入 memory-read snapshot 条件，尝试处理只读局部内存；
5. 建立 region verifier，拒绝可能改变 concrete semantics 的合成。

挑战：

- alias analysis 精度不足时必须保守；
- LLVM poison/undef/freeze 语义需要显式处理；
- 复杂 region 可能增加公式规模，反而降低求解效率。

### P1：UCSan 对象图 seed synthesis

目标：把 under-constrained execution 从“结构化 seed replay”推进到“对象图生成”。

任务：

1. 设计 object graph grammar；
2. 支持 pointer alias、shared subobject、cycle；
3. 从 crash-free concrete replay 中学习对象形状；
4. 将 LLM/agentic route 用于 object seed mutation；
5. 对函数入口覆盖和全程序 fuzzing 覆盖做联合评价。

挑战：

- pointer validity 与 symbolic pointer arithmetic 的平衡；
- 外部函数 stub 的 soundness；
- seed 空间爆炸与 object graph 最小化。

### P1：SymSan/taint backend 对照实验

目标：验证“表达式构造”和“taint 传播解耦”对当前 coordinator 的收益。

任务：

1. 统一 SymCC 与 SymSan telemetry schema；
2. 同一 AFL/coordinator 下切换 backend；
3. 对比 runtime overhead、coverage、solver query quality；
4. 将 comparison taint 和 focus_set 从 backend-specific 迁移到 engine-neutral 层。

挑战：

- backend 语义差异导致 telemetry 不完全等价；
- taint-only 路径可能生成更少 SMT 表达式，但也可能丢失精确求解机会。

### P2：学习型调度从 bandit 推进到因果/离线强化学习

目标：让调度器学到“哪个 seed-state-route 在当前 corpus 下真正增加覆盖”。

任务：

1. 收集 offline trajectory dataset；
2. 构建 counterfactual replay simulator；
3. 对 LinUCB、Thompson sampling、contextual MDP、offline RL 做比较；
4. 引入 uncertainty-aware route selection；
5. 研究 worker redundancy 作为负 reward 的建模方式。

挑战：

- fuzzing 环境非平稳；
- 同一 action 的收益依赖 concurrent workers；
- offline policy 容易过拟合 benchmark。

### P2：面向论文的系统化理论抽象

目标：将工程系统抽象为一套可解释的模型，提升学术贡献清晰度。

可能抽象：

```text
Hybrid symbolic fuzzing = coverage-guided stochastic search
                         + constraint-guided state transition
                         + distributed continuation scheduling
                         + verified neural/agentic proposal.
```

需要形式化的问题：

- continuation state 的等价关系；
- prefix context reuse 的 soundness 边界；
- verified LLM proposal 的 acceptance criterion；
- data coverage 与 code coverage 的联合 dominance。

## 六、预期论文结构

一个可能的论文框架：

1. Introduction：并行 hybrid fuzzing 的冗余和结构化输入瓶颈；
2. Motivation：三个 motivating examples：
   - implicit flow；
   - solver-hostile structured parser；
   - multi-worker duplicate continuation；
3. Design：
   - compiler/runtime telemetry；
   - prefix DAG/actionseed；
   - state shard coordinator；
   - agentic route；
4. Implementation：SymCC/QSYM/AFL/MPI 细节；
5. Evaluation：
   - coverage；
   - scaling；
   - ablation；
   - overhead；
   - route quality；
6. Discussion：
   - soundness boundary；
   - LLM verification；
   - limitations；
7. Related Work：
   - QSYM/SymCC/SymSan；
   - Pangolin；
   - Backsolver；
   - Veritesting；
   - GenSym；
   - Cottontail/ConcoLLMic/Gordian；
   - directed hybrid fuzzing。

## 七、参考文献与技术来源

- Backsolver: Adapting Preceding Execution Paths to Solve Constraints, ACM TOSEM 2025. https://dl.acm.org/doi/10.1145/3712194
- Enhancing Symbolic Execution with Veritesting, ICSE 2014. https://dl.acm.org/doi/10.1145/2568225.2568293
- GenSym: Compiling Parallel Symbolic Execution with Continuations, ICSE 2023. https://dl.acm.org/doi/10.1109/ICSE48619.2023.00116
- Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction, IEEE S&P 2020. https://doi.org/10.1109/SP40000.2020.00063
- Cottontail: Large Language Model-Driven Concolic Execution for Highly Structured Test Input Generation, IEEE S&P 2026. https://mboehme.github.io/paper/SP26-cottontail.pdf
- ConcoLLMic: Agentic Concolic Execution, IEEE S&P 2026. https://github.com/ConcoLLMic/ConcoLLMic
- Gordian: LLM-assisted hybrid symbolic execution with ghost code, 2026 preprint. https://arxiv.org/html/2603.19239v1
- Data Coverage for Guided Fuzzing, USENIX Security 2024. https://www.usenix.org/conference/usenixsecurity24/presentation/wang-mingzhe
- MultiGo: Not All Paths Are Equal, ACM TOSEM 2025. https://dl.acm.org/doi/10.1145/3735555
- TACO-Fuzz: Efficient Directed Hybrid Fuzzing via Target-Centric Seed Selection and Generation, OOPSLA 2026. https://2026.splashcon.org/details/oopsla-2026/35/Efficient-Directed-Hybrid-Fuzzing-via-Target-Centric-Seed-Selection-and-Generation

## 八、近期验证状态

最近一次完整验证结果：

- `cmake --build build --target SymCC SymCCRuntime -j2`：通过；
- `python3 -m unittest discover -s test -p 'test_*.py'`：70 个测试通过；
- `lit --path=/usr/lib/llvm-18/bin -v build/test`：53 个 lit 测试通过。

这些测试覆盖 compiler instrumentation、Backsolver/Veritesting、UCSan seed、
S2F actionseed、AFL data coverage、distributed state、agentic hooks、hybrid feedback
和核心运行时集成。