aravinth-kanesh/polyml-fuzz

# Poly/ML 编译器模糊测试（ARM64） 一个用于在 ARM64 上测试 Poly/ML 编译器前端的基于覆盖率引导的模糊测试框架，作为伦敦国王学院（King's College London）本科毕业设计项目。 **动机：** Poly/ML 是 Isabelle/HOL 证明助手的核心组件，构成了其可信计算基础的一部分。本项目建立了首个针对 ARM64 上 Poly/ML 的系统性基于模糊测试的可靠性基线。 **范围：** 词法分析与语法解析（仅限编译器前端）。 **工具：** AFL++、AddressSanitizer、UndefinedBehaviorSanitizer、LLVM 源代码覆盖率。 **报告：** [aravinth-kaneshalingam-fyp-report](https://github.com/aravinth-kanesh/aravinth-kaneshalingam-fyp-report) ## 快速开始 ``` # 在 AWS Graviton (Ubuntu 22.04 ARM64) 或任何 ARM64 Linux 机器上： git clone https://github.com/aravinth-kanesh/polyml-fuzz.git polyml-fuzz cd polyml-fuzz # 一键式安装：安装工具，构建 poly，验证并验证种子 ./setup.sh # 交互式向导：配置阶段、持续时间、实例，然后启动 ./fuzz.sh ``` `setup.sh` 处理所有依赖并构建。`fuzz.sh` 引导你完成整个活动周期，包括活动后分析和第 1 阶段到第 2 阶段语料库的交接。 ## 仓库结构 ``` polyml-fuzz/ |-- setup.sh # One-command setup (run this first on a fresh clone) |-- fuzz.sh # Interactive wizard: configure and launch campaigns |-- Makefile # Named targets: make smoke / phase1 / phase2 / report |-- harness/ | \-- main.c # Initial harness design (reference only; not used in campaigns) |-- seeds/ # 72 SML seed programs | |-- basic/ # Core language features (12 seeds, Phase 1) | |-- operators/ # Infix, precedence, fixity (11 seeds, Phase 1) | |-- edge-cases/ # Lexer boundary cases, numeric literals ( 9 seeds, Phase 1) | |-- regression/ # Known UBSan-triggering seeds ( 3 seeds, Phase 1) | |-- stress/ # Deep nesting, long identifiers (14 seeds, Phase 2) | |-- modules/ # Structures, signatures, functors (12 seeds, Phase 2) | \-- datatypes/ # ADTs, pattern matching, records (11 seeds, Phase 2) |-- scripts/ | |-- ec2-setup.sh # AWS ARM64 system dependency installer | |-- build-polyml.sh # Build AFL++-instrumented Poly/ML | |-- build-polyml-coverage.sh # Build LLVM coverage-instrumented Poly/ML (for analysis) | |-- build-harness.sh # Build harness binary (reference only) | |-- coverage-report.sh # Generate per-file LLVM source coverage report | |-- verify-build.sh # Verify AFL++ instrumentation is active | |-- validate-seeds.sh # Run all 72 seeds through poly | |-- prepare-evolved-seeds.sh # Copy Phase 1 queue for use as Phase 2 seeds | |-- fetch-isabelle-seeds.sh # Extract SML seeds from Isabelle source | |-- sml_mutator.py # Grammar-aware AFL++ custom mutator | \-- trim-seeds.sh # Minimise large seeds with afl-tmin |-- campaign/ | |-- start.sh # tmux launcher: opens fuzzer, monitor, and analytics panes | |-- launch.sh # Core AFL++ campaign launcher (called by start.sh) | |-- monitor.sh # Live coverage/crash dashboard | |-- analytics.sh # Edges/hour logging and saturation detection | |-- analyse.sh # Post-campaign one-liner: crashes + triage + report + coverage | |-- collect-crashes.sh # Deduplicate and minimise crashes | |-- triage.sh # Reproduce and classify crashes by fault type | |-- reproduce-crash.sh # Standalone single-crash reproduction tool | \-- report.sh # Generate Markdown campaign summary |-- results/ | \-- early-findings/ # Bugs found before the main campaign |-- docs/ # Supporting documentation \-- build/ # Build outputs (gitignored) ``` 外部依赖（在 Linux 上由 `./setup.sh` 自动克隆）： - `AFLplusplus/`：[github.com/AFLplusplus/AFLplusplus](https://github.com/AFLplusplus/AFLplusplus) - `polyml-src/`：[github.com/polyml/polyml](https://github.com/polyml/polyml) ## 安装 ### 在 AWS Graviton 或任何 ARM64 Linux 机器上 ``` git clone https://github.com/aravinth-kanesh/polyml-fuzz.git polyml-fuzz && cd polyml-fuzz ./setup.sh ``` `setup.sh` 运行五个步骤，并跳过已完成的部分，因此可以安全地重新运行： 1. 安装系统包（clang-15、AFL++、autoconf 2.72、构建工具） 2. 构建 AFL++ 插桩的 `poly` 二进制文件 3. 验证 AFL++ 插桩在二进制文件中处于激活状态 4. 验证所有 72 个种子（预期：71 通过，1 超时，0 崩溃） 5. 构建用于活动后分析的 LLVM 覆盖率插桩 `poly` 二进制文件 ### 在 macOS 上（仅用于验证） 由于共享内存限制，AFL++ 持久模式在 macOS 上无法工作。你可以在本地构建以验证种子，但所有模糊测试活动必须在 Linux ARM64 上运行。 在运行 `./setup.sh` 之前，你需要手动克隆 `AFLplusplus/` 和 `polyml-src/`。 ## 运行活动 ### 交互式向导（推荐） ``` ./fuzz.sh ``` 该向导会提示输入阶段、持续时间和实例数量，然后在一个包含三个窗口的 tmux 会话中启动活动：模糊器、实时监控和分析日志记录。活动结束时，它会自动运行活动后分析并提供启动第 2 阶段的选项。 ### Make 目标 ``` make smoke # 30-minute validation run (Phase 1, 1 instance) make phase1 # Full Phase 1 campaign (3 days, 4 instances) make phase2 # Phase 2 without evolved seeds make phase2 EVOLVED=phase1-lexer-YYYYMMDD-HHMMSS # Phase 2 with Phase 1 corpus make monitor CAMPAIGN=phase1-lexer-YYYYMMDD-HHMMSS # Live dashboard make report CAMPAIGN=phase1-lexer-YYYYMMDD-HHMMSS # Re-run post-campaign analysis ``` ### 手动启动 ``` ./campaign/start.sh --phase 1 --duration 259200 --instances 4 ``` ## 活动策略 两个连续的 3-4 天阶段，每个阶段针对不同的种子子集。 ### 第 1 阶段：词法分析器重点（子集 A） 种子：`basic/`、`operators/`、`edge-cases/`、`regression/` 这些用于测试词法分析器：标记化、操作符、字面量、嵌套注释和边界值。 ### 第 2 阶段：解析器重点（子集 B，条件性） 种子：`stress/`、`modules/`、`datatypes/` 这些用于测试解析器，处理深度嵌套、模块层次结构、复杂类型和函子应用。仅在活动 1 产生有效结果后运行。第 2 阶段使用缩短的超时（5000ms）、对模糊器 01 和 02 启用 CMPLOG 插桩以辅助魔字节求解，并在模糊器 03 上使用 `rare` 调度策略以多样化边缘探索。 当通过 `fuzz.sh` 启动时，第 1 阶段完成后会自动提供第 2 阶段，并可选择从第 1 阶段的演化语料库为其播种。在启动第 2 阶段之前，可选择执行可选的 `afl-cmin` 最小化步骤。 ### 语法感知变异器（可选） 一个自定义 AFL++ 变异器（`scripts/sml_mutator.py`）应用结构感知的 SML 变异，例如病态浮点字面量、长标识符和嵌套表达式变体。通过以下方式启用： ``` ./campaign/launch.sh --phase 2 --grammar-mutator --duration 259200 --instances 4 ``` ### 饱和度 当每小时发现的新边少于 10 条且连续 3 小时发生时，声明覆盖率饱和。`analytics.sh` 会自动跟踪此信息并记录到 `results//analytics/saturation.log`。 ## 活动后分析 当活动通过 `fuzz.sh` 或 `campaign/start.sh` 结束时，分析会自动运行。也可手动运行： ``` ./campaign/analyse.sh ``` 这按顺序执行四个步骤： 1. 收集并去重崩溃（SHA-256 去重，然后使用 `afl-tmin` 最小化） 2. 对每个崩溃进行诊断（重现、按故障类型分类：UBSan / ASan / 信号） 3. 生成 `results//REPORT.md`，包含覆盖率、崩溃数量和语料库统计信息 4. 对演化语料库运行 LLVM 源代码覆盖率，将每个文件的结果写入 `results//coverage/` 报告包含 `libpolyml/` 区域的总覆盖率，以及如果构建了覆盖率二进制文件，则包含 `arm64.cpp` 的覆盖率。 ## 崩溃重现 ``` # 从 AFL++ 输出目录重现崩溃 ./campaign/reproduce-crash.sh results//fuzzer01/crashes/id:000001,sig:06,... # 手动重现 ASAN_OPTIONS=halt_on_error=1:abort_on_error=1 \ UBSAN_OPTIONS=print_stacktrace=1 \ poly < ``` ## 发现 在预活动验证和两个生产活动中确认了四个可靠性问题。截至 2026 年 4 月，Polyml 源代码仓库中仍有三个未解决；问题 3 的阶段 2 模块展开缺陷（崩溃 1 和 2）在提交 `cf7b84a` 中由 Poly/ML 开发团队确认并修复。 **发现 1 - ARM64 特定的 UBSan 整数溢出（预活动）** `libpolyml/arm64.cpp:246`（当前上游主版本中的第 440 行）的 UBSan 无符号整数溢出。由两个有效的 SML 程序触发：在 x86-64 上执行相同程序不会产生输出。 ``` poly < results/early-findings/ub1/inputs/seed_fun.sml poly < results/early-findings/ub1/inputs/seed_datatype.sml ``` 一行修复（将除数强制转换为 `POLYSIGNED`）已在本地验证，但尚未合并到上游。 **发现 2 - 词法分析器在病态浮点字面量上的无限制内存分配（阶段 1）** `LEX_.ML` 中的 `readChars` 在读取浮点字面量中 `e`/`E` 后的指数数字时没有长度限制。指数位数百个数字会导致内存分配与长度成正比（确认无需 ASan：200 位数字 → 20 MB，1,000,000 位数字 → 192 MB）。已通过限制（`readCharsMax`，上限为 20 位）在本地验证修复。错误报告已提交至 Poly/ML 邮件列表；分类为缺陷尚待维护者确认。 **发现 3 - 模块展开 SIGSEGV：带有损坏标识符的嵌套结构（阶段 2）** 两个独立发现的 AFL++ 输入在 AFL++ 变异破坏嵌套几何模块中的结构名称时触发模块展开代码中的 SIGSEGV。根本原因：`TYPE_TREE.ML` 中重载解析的类型安全缺陷——`OverloadSetVar` 未在函数声明时提交，导致使用浮点参数调用时出现类型不匹配崩溃。最小化重现程序：`fun ma x y = (x - y); ma 0.0 0.0`。 **发现 4 - 模块展开 SIGSEGV：值绑定中整数字面量模式（阶段 2）** 一个包含 `val 0 = 0` 的 80 字节结构定义会触发 SIGSEGV。解析器接受该整数字面量模式而不出错，但展开器在处理时会崩溃。重现程序： ``` structure Mat0 = struct val 0 = 0 fun s0uare x = x+x fun e 0 = () end; val a = Mat0.s0uare 0.0 ``` 完整的崩溃输入、诊断报告和 LLVM 覆盖率报告位于 `results/findings/`。有关活动摘要，请参见 `results/findings/README.md`。 ## AFL++ 变异策略 | 变异器 | 对 SML 的影响 | |--------|---------------| | 位/字节翻转 | 破坏单个标记字符 | | 算术 | 扰动整数字面量 | | 有趣的值 | 在字节边界替换 0、MAX_INT、-1 | | 拼接 | 将语料库条目重新组合为语法混合体 | | 混乱 | 将上述随机变异堆叠 | 通过 `-x` 传递 SML 令牌字典（`seeds/sml.dict`）以补充混乱变异中的关键字和运算符替换。使用 `-a text` 标志使变异偏向可打印 ASCII 字符。 ## 故障排除 **`afl-clang-lto` 未找到** ``` cd AFLplusplus && make distclean && make ``` **macOS 上的 `shmget()` 失败** 在 Linux ARM64 上运行活动。macOS 系统 V 共享内存限制会阻止 AFL++ 持久模式运行。 **0 exec/sec** ``` ./scripts/validate-seeds.sh # confirm the binary and seeds work ./scripts/verify-build.sh # confirm AFL++ instrumentation is active ``` **覆盖率报告显示“未生成”** ``` ./scripts/build-polyml-coverage.sh # or re-run ./setup.sh ```

标签：AFL++, ARM64, ASan, BSc 毕设, Fuzzing, Fuzzing Framework, ISCAS, King's College London, LLVM 源码覆盖率, Poly/ML, UBSan, 代码安全, 内核测试, 可靠性基线, 地址消毒剂, 子域名枚举, 客户端加密, 未定义行为消毒剂, 漏洞枚举, 系统安全, 编译前端, 编译器, 覆盖率引导, 逆向工具