dfs333/trivycompromiseanalysis

# 多阶段 CI/CD 供应链攻击的定量分析 对 2026 年 3 月 Trivy / “TeamPCP” GitHub Actions 供应链破坏事件（**CVE-2026-33634**）进行的**经过形式化验证的定量重建**——使用 TLA+ 建模，通过 TLC 进行 详尽检查，并使用 PRISM 概率模型检测器进行量化。     [](https://github.com/dfs333/trivysupplychainanalysis/actions/workflows/verify.yml) [](https://doi.org/10.5281/zenodo.21387135) ## 发生了什么，以及这证明了什么 攻击者通过移动一个被广泛使用的 Action（`trivy-action` / `setup-trivy`）上的浮动版本标签，导致数千个下游流水线在下一次例行运行时，携带生产凭证执行了攻击者控制的 代码，泄露的机密信息随后为第二阶段的 npm 蠕虫提供了种子。本项目提出了事件报告无法在形式上回答的问题： - **完全轮换与部分凭证轮换。** 模型证明了实际发生的*部分* 轮换**并未**阻断攻击，而*完全*轮换则可以——这与记录在案的事件起因相符。 - **SHA 绑定隔离了流水线。** 绑定了 commit-SHA 的流水线被证明绝对不会 被攻陷，*即使其相邻流水线被攻陷，甚至即使被盗凭证仍然 有效*——破坏仅局限于未绑定的子集（一个形式化的隔离定理 + 一个量化残余攻击面的精化关系）。 - **可能性有多大，速度有多快，影响有多广。** 精确的攻陷概率、预期的 攻陷时间、两阶段 npm 传播级联，以及封闭形式的参数化 结果，均根据真实的恶意软件包频率数据进行校准。 - **该发现经受住了自动化搜索的考验。** 一个 LLM 提议者（Claude Opus 4.8）在 防御者策略空间中针对已验证的 PRISM 预言机进行搜索，最终在无人类 指导的情况下——收敛于相同的最低成本且可证明安全的策略：轮换残余凭证。 提议者负责建议；模型检测器负责决策。 ## 关键结果 | 问题 | 结果 | |---|---| | 记录在案的攻击是否可达？ | **是** —— TLC 返回了精确的 3 步档案追踪 | | 部分轮换是否足够？ | **否**（`NoExfiltration` 失败）；完全轮换**可以** | | 混合环境中的 SHA 绑定 | **隔离成立**，覆盖 8,185 个状态；破坏被遏制 | | P(攻陷)，脆弱配置 | **1.0**；E[时间] **6 天**；P(≤30 天) **0.9985** | | 多阶段级联 | P(达到阶段 2) **= q**；E[首个下游] **16 天**；**轮换 → 0** | | 参数化（封闭形式） | E[攻陷天数] **= (p+1)/p**；P(阶段 2) **= q**（精确值） | | 层 1 语料库（189 个真实工作流） | 浮动标签比例 **f = 0.3698**；构造覆盖率 **88.2%** | | 校准（OpenSSF/OSV） | npm = 214,497 份报告 (94.2%)；**2026 年 2 月→3 月：329 → 1,048 (×3.19)** | | 自动化缓解搜索 | LLM 提议，PRISM 验证 → **仅轮换最优**（得分 -0.05），在 4 轮内收敛 | ## 三层验证 1. **结构忠实度**（`TrivySupplyChain/layer1/`）—— 对真实 GitHub Actions 工作流 语料库进行静态分析，测量所建模构造的出现频率 （14/14 单元测试；浮动标签比例馈入层 3）。 2. **事件重建**（`TrivySupplyChain/`）—— TLA+ 模型 + 10 个 TLC 配置重现了攻击，并证明了哪些缓解措施可以阻断它（可达性、 隔离、精化、残余面）。 3. **预测性校准**（`TrivySupplyChain/layer3/`）—— PRISM MDP/DTMC 计算 概率、预期时间以及多阶段级联，并根据 OpenSSF 恶意软件包数据集和记录在案的 2 月→3 月时间线进行了校准。 ## 仓库布局 ``` TrivySupplyChain/ The model + verification harness TrivySupplyChain.tla Core TLA+ transition system MCTrace.tla, SecureWorkflow.tla, MCRefine.tla cfg_*.cfg 10 TLC configurations (the validation table) tools/tla2tools.jar Bundled TLA+ / TLC 2.19 layer1/ Corpus analyzer (Python) + fixtures + tests layer3/ PRISM models (.prism/.props) + bundled PRISM 4.10.1 asi_evolve/ LLM mitigation-search loop (run_evolve.py) over the verified PRISM oracle + an archived executed run (example_run.json) run-all.ps1 Reproduce all 10 TLC checks env-check.ps1 One-shot environment doctor Trivy-USENIX-paper/ USENIX paper: main.tex (compiles standalone), main.pdf, and the filled-in validation-results .docx Trivy-TeamPCP-Dossier.md Incident dossier — the sourced evidence base (read-only) ``` ## 复现指南 **环境要求：** Windows + JDK（设置 `JAVA_HOME`）；Python 3.10+（层 1 和校准）； Node.js（仅用于重新生成 Word 文档）；Git for Windows（提供 PRISM 原生库所需的 MinGW 运行时 DLL）。TLA+ 工具和 PRISM **已捆绑**在此仓库中。 ``` # 0. 验证 toolchain powershell -File TrivySupplyChain\env-check.ps1 # 1. Layer 2 — 全部 10 项 TLC 检查（可达性、缓解措施、隔离、细化） powershell -File TrivySupplyChain\run-all.ps1 # 2. Layer 1 — 语料库分析（单元测试 + 测量的 floating-tag 比例） powershell -File TrivySupplyChain\layer1\run-layer1.ps1 # 3. Layer 3 — PRISM：概率、多级联、参数化、校准 powershell -File TrivySupplyChain\layer3\run-layer3.ps1 # 4. （可选）ASI-Evolve 缓解策略搜索 — Claude Opus 提出策略， # PRISM 验证每一个。需要 Anthropic SDK + 一个 API key。 pip install -r TrivySupplyChain\asi_evolve\requirements.txt python TrivySupplyChain\asi_evolve\run_evolve.py ``` 层 1–3 是自包含的，无需任何 API 密钥。只有第 4 步的*提议者*是 LLM； 它的 PRISM 预言机（`asi_evolve/evaluate.py`）可独立运行，也是实际对 各项策略进行评分的组件。 `.tla`、`.prism` 和 `.py` 源代码是可移植的；只有运行脚本是 Windows PowerShell。请参阅 `TrivySupplyChain/README.md` 获取手动（跨平台）命令。 ## 论文 `Trivy-USENIX-paper/main.tex` 是采用 USENIX Security 双栏格式的正式文稿。它是 自包含的（标准的 CTAN 宏包），可以在 Overleaf 或任何 TeX 引擎上编译： ``` pdflatex main.tex && pdflatex main.tex # or: tectonic main.tex ``` 编译后的论文是 `main.pdf`；填写好的验证报告（Word）是 `QA -- Validation Results (Filled In).docx` —— 两者均位于 `Trivy-USENIX-paper/` 中。 ## 分支 - **`main`** —— 当前修正后的分析。请从此处构建。 - **`pre-mercor-fix`** —— 在 Mercor→v1 重新标记之前该项目的存档重建（Mercor 的破坏是通过阶段 2 的 LiteLLM 后续跟进发生的，而不是直接的 trivy-action 执行）。仅供参考；请查看该分支上的 `PRE-MERCOR-FIX.md`。 ## 状态与范围 由 **Franklin Hanna** 撰写的研究预印本正在进行中（隶属机构/电子邮件在 `main.tex` 中仍是占位符）。事件 事实取自公开档案（Aqua、GHSA、CVE-2026-33634、Unit 42、Microsoft、 Wiz、ReversingLabs、Endor Labs、OpenSSF/OSV 等）。建模假设及其 局限性在论文的*局限性与有效性威胁*部分有明确说明。 ## 引用 如果您使用了这项工作，请引用归档发布版本（Zenodo DOI [10.5281/zenodo.21387135](https://doi.org/10.5281/zenodo.21387135)）；机器可读的 元数据位于 [`CITATION.cff`](CITATION.cff) 中。 ``` @software{hanna_2026_trivy_teampcp, author = {Hanna, Franklin}, title = {Formal Analysis of the Trivy / TeamPCP GitHub Actions Supply-Chain Attack (CVE-2026-33634)}, year = {2026}, version = {v1.0.0}, publisher = {Zenodo}, doi = {10.5281/zenodo.21387135}, url = {https://doi.org/10.5281/zenodo.21387135} } ``` ## 许可证 - **代码与形式化方法产物**（分析器、TLA+/PRISM 模型、脚本、生成器）—— [Apache License 2.0](LICENSE)。 - **论文文本及其呈现形式**（`Trivy-USENIX-paper/`）—— [CC BY 4.0](Trivy-USENIX-paper/LICENSE)。 捆绑的第三方工具保留其各自的许可证：PRISM 为 GPL （`TrivySupplyChain/layer3/prism/COPYING.txt`），TLA+ 工具为 MIT。

标签：AI合规, CI/CD安全, DevSecOps, JS文件枚举, Llama, StruQ, 上游代理, 形式化验证, 文档安全, 漏洞分析, 路径探测, 软件开发工具包, 逆向工具