dfs333/trivysupplychainanalysis形式的に検証された、Trivy/TeamPCPのGitHub Actionsサプライチェーン攻撃（CVE-2026-33634）の定量的再構築：TLA+/TLCインシデントモデル、PRISM確率解析、および189ワークフローコーパス研究。
形式的に検証され、定量的に再構築された2026年3月のTrivy / "TeamPCP" GitHub Actionsサプライチェーン侵害（CVE-2026-33634）— TLA+でモデル化し、TLCで網羅的にチェックし、PRISM確率モデル検査器で定量化。
論文内のすべての数値はこのリポジトリから再生成されます。 モデル、確率、コーパス測定、キャリブレーションはすべて、ソースから各レイヤーごとに単一のコマンドで再現可能です。
広く使われているAction（trivy-action / ）上の浮動バージョンタグを移動できた攻撃者は、何千もの下流パイプラインが次回の定期実行時に攻撃者の制御するコードを実稼働認証情報とともに実行するように仕向け、シークレットを漏洩させ、それが第二段階のnpmワームの基となりました。このプロジェクトは、インシデントレポートが形式的に答えられない質問を問います。
setup-trivy| 質問 | 結果 |
|---|---|
| 文書化された攻撃は到達可能か？ | はい — 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ラウンドで収束 |
TrivySupplyChain/layer1/) — 実際のGitHub Actionsワークフローのコーパスに対する静的解析器が、モデル化された構造がどの程度の頻度で出現するかを測定（14/14単体テスト；浮動タグ割合はレイヤー3に供給）。TrivySupplyChain/) — TLA+モデル + 10のTLC構成が攻撃を再現し、どの軽減策が攻撃を封じるかを証明（到達可能性、分離、精緻化、残存表面）。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の侵害は直接のtrivy-action実行ではなく、ステージ2のLiteLLMフォローオン経由でした）。参考用のみ；そのブランチの PRE-MERCOR-FIX.md を参照してください。Franklin Hanna による研究中のプレプリント（所属/メールは main.tex 内でまだプレースホルダーです）。インシデントの事実は公開調査報告書（Aqua、GHSA、CVE-2026-33634、Unit 42、Microsoft、Wiz、ReversingLabs、Endor Labs、OpenSSF/OSVなど）から引用しています。モデル化の前提とその限界は、論文の Limitations and Threats to Validity セクションで明示的に述べられています。
この研究を使用する場合は、アーカイブ済みリリース（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}
}
Trivy-USENIX-paper/) — CC BY 4.0.バンドルされたサードパーティツールはそれぞれのライセンスに従います：PRISMはGPL（TrivySupplyChain/layer3/prism/COPYING.txt）、TLA+ツールはMITです。