多阶段CI/CD供应链攻击的定量分析

一个经过形式化验证、定量重建的2026年3月Trivy / "TeamPCP" GitHub Actions供应链入侵事件（CVE-2026-33634）——在TLA+中建模，由TLC穷举检查，并通过PRISM概率模型检验器量化。

论文中的每一个数字都从这个仓库重新生成。 模型、概率、语料库测量和校准结果均可从源码通过每层一个命令重现。

事件经过与本研究证明的内容

攻击者能够移动一个广泛使用的Action（trivy-action / setup-trivy）上的浮动版本标签，导致数千个下游管道在其下一次例行运行时执行攻击者控制的代码，并使用生产凭证泄露机密，从而引发了第二阶段的npm蠕虫。本项目提出了事件报告无法正式回答的问题：

• 完整 vs. 部分凭证轮换。 模型证明实际发生的部分轮换无法封闭攻击，而完整轮换可以——与记录的事件因果关系一致。
• SHA固定隔离管道。 使用提交SHA固定的管道可证明永远不会被入侵，即使其相邻管道被入侵且被盗凭证仍然有效——入侵被限制在未固定子集内（一个形式化的隔离定理 + 一个量化残余攻击面的细化关系）。
• 可能性、速度、范围。 精确的入侵概率、预期入侵时间、两阶段npm传播级联以及封闭形式参数化结果，已根据真实恶意包频率数据进行校准。
• 发现结果经得起自动搜索。 一个LLM提议器（Claude Opus 4.8）在针对已验证的PRISM预言机搜索防御策略空间时，在无人类引导下收敛到了相同的最小代价可证明安全策略：轮换残余凭证。提议器提出建议；模型检查器做出决策。

关键结果

三层验证

1. 结构忠实性（TrivySupplyChain/layer1/）——一个针对真实GitHub Actions工作流泪语料库的静态分析器，测量建模结构出现的频率（14/14单元测试；浮动标签占比输入第3层）。
2. 事件重建（TrivySupplyChain/）——TLA+模型 + 10个TLC配置重现攻击并证明哪些缓解措施能封闭攻击（可达性、隔离、细化、残余表面）。
3. 预测校准（TrivySupplyChain/layer3/）——PRISM MDP/DTMC计算概率、预期时间和多阶段级联，已根据OpenSSF恶意包数据集和文档记录的2月→3月时间线进行校准。

仓库布局

TrivySupplyChain/            模型 + 验证工具链
  TrivySupplyChain.tla       核心TLA+转换系统
  MCTrace.tla, SecureWorkflow.tla, MCRefine.tla
  cfg_*.cfg                  10个TLC配置（验证表）
  tools/tla2tools.jar        捆绑的TLA+ / TLC 2.19
  layer1/                    语料库分析器（Python）+ 测试夹具 + 测试
  layer3/                    PRISM模型（.prism/.props）+ 捆绑的PRISM 4.10.1
  asi_evolve/                LLM缓解措施搜索循环（run_evolve.py），基于已验证的PRISM预言机 + 存档的执行运行（example_run.json）
  run-all.ps1                重现所有10个TLC检查
  env-check.ps1              一键环境诊断
Trivy-USENIX-paper/          USENIX论文：main.tex（可独立编译）、main.pdf、以及已填写的验证结果.docx
Trivy-TeamPCP-Dossier.md     事件档案——基于来源的证据库（只读）

layer2/在哪儿？ 第2层（事件重建）就是TrivySupplyChain/的顶层——TrivySupplyChain.tla模型、cfg_*.cfg配置、MC*.tla/SecureWorkflow.tla模块以及run-all.ps1。它首先作为核心构建，因此位于根目录；layer1/和layer3/是后来添加的验证层。

重现方法

要求： Windows + JDK（设置JAVA_HOME）；Python 3.10+（第1层和校准）；Node.js（仅用于重新生成Word文档）；Git for Windows（提供PRISM原生库所需的MinGW运行时DLL）。TLA+工具和PRISM已捆绑在仓库中。

# 0. 验证工具链
powershell -File TrivySupplyChain\env-check.ps1

# 1. 第2层——所有10个TLC检查（可达性、缓解措施、隔离、细化）
powershell -File TrivySupplyChain\run-all.ps1

# 2. 第1层——语料库分析（单元测试 + 测量的浮动标签占比）
powershell -File TrivySupplyChain\layer1\run-layer1.ps1

# 3. 第3层——PRISM：概率、多阶段级联、参数化、校准
powershell -File TrivySupplyChain\layer3\run-layer3.ps1

# 4. （可选）ASI-Evolve缓解措施搜索——Claude Opus提议策略，PRISM逐一验证。需要Anthropic SDK + API密钥。
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。

第3层按捆绑方式仅支持Windows。 PRISM在此以原生Windows库（prism.dll、CUDD）以及Git-for-Windows MinGW运行时形式提供，因此run-layer3.ps1仅在Windows上运行。Linux/macOS审阅者无法从捆绑二进制运行第3层——但.prism/.props模型是可移植的：安装上游PRISM（https://www.prismmodelchecker.org）并直接运行，例如prism layer3/trivy_mdp.prism layer3/trivy.props。第1–2层是跨平台的（Python，且捆绑的tla2tools.jar可在任何装有JDK的系统上运行）。

论文

📄 在浏览器中阅读： main.pdf——GitHub内联渲染。直接下载链接附在v1.0.0版本中。

Trivy-USENIX-paper/main.tex是以USENIX Security双栏格式撰写的文章。它是自包含的（标准CTAN包），可在Overleaf或任何TeX引擎上编译：

pdflatex main.tex && pdflatex main.tex     # 或：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）；机器可读元数据在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许可证2.0版。
• 论文文本及其呈现（Trivy-USENIX-paper/）——CC BY 4.0。

捆绑的第三方工具保留其各自许可证：PRISM为GPL（TrivySupplyChain/layer3/prism/COPYING.txt），TLA+工具为MIT。