dfs333/trivysupplychainanalysisFormal verifizierte, quantitative Rekonstruktion des Supply-Chain-Angriffs auf Trivy/TeamPCP GitHub Actions (CVE-2026-33634): ein TLA+/TLC-Vorfallmodell, PRISM-Wahrscheinlichkeitsanalyse und eine Korpusstudie mit 189 Workflows.
Eine formal verifizierte, quantitative Rekonstruktion der GitHub-Actions-Supply-Chain-Kompromittierung von Trivy / „TeamPCP" vom März 2026 (CVE-2026-33634) — modelliert in TLA+, erschöpfend mit TLC geprüft und quantifiziert mit dem probabilistischen Modellprüfer PRISM.
Jede Zahl im Paper wird aus diesem Repository neu erzeugt. Das Modell, die Wahrscheinlichkeiten, die Korpusmessungen und die Kalibrierung lassen sich jeweils mit einem einzigen Befehl pro Ebene aus dem Quellcode reproduzieren.
Ein Angreifer, der ein gleitendes Versions-Tag einer weit verbreiteten Action (trivy-action
/ setup-trivy) verschieben konnte, führte dazu, dass Tausende nachgelagerter Pipelines beim
nächsten Routine-Lauf Angreifer-kontrollierten Code mit Produktions-Anmeldedaten ausführten,
wodurch Geheimnisse geleakt wurden, die einen npm-Wurm der zweiten Stufe auslösten. Dieses
Projekt stellt die Fragen, die ein Incident-Bericht nicht formal beantworten kann:
| Frage | Ergebnis |
|---|---|
| Ist der dokumentierte Angriff erreichbar? | Ja — TLC liefert die exakte 3-Schritte-Spur des Dossiers |
| Reicht eine teilweise Rotation? | Nein (NoExfiltration schlägt fehl); vollständige Rotation ja |
| SHA-Pinning in einer gemischten Population | Isolation gilt über 8,185 Zustände; Vorfall eingedämmt |
| P(Kompromittierung), verwundbare Konfiguration | 1.0; E[Zeit] 6 Tage; P(≤30 Tage) 0.9985 |
| Mehrstufige Kaskade | P(Stufe 2 erreichen) = q; E[erste nachgelagerte Pipeline] 16 Tage; Rotation → 0 |
| Parametrisch (geschlossene Form) | E[Tage bis Kompromittierung] = (p+1)/p; P(Stufe 2) = q (exakt) |
| Layer-1-Korpus (189 echte Workflows) | Anteil gleitender Tags f = 0.3698; Konstrukt-Abdeckung 88.2% |
| Kalibrierung (OpenSSF/OSV) | npm = 214,497 Meldungen (94.2%); Feb→Mär 2026: 329 → 1,048 (×3.19) |
| Automatisierte Suche nach Gegenmaßnahmen | LLM schlägt vor, PRISM verifiziert → reines Rotations-Optimum (Score −0.05), in 4 Runden konvergiert |
TrivySupplyChain/layer1/) — ein statischer Analysator
misst anhand eines Korpus echter GitHub-Actions-Workflows, wie häufig die modellierten
Konstrukte vorkommen (14/14 Unit-Tests; der Anteil gleitender Tags fließt in Layer 3 ein).TrivySupplyChain/) — das TLA+-Modell plus 10
TLC-Konfigurationen reproduzieren den Angriff und beweisen, welche Gegenmaßnahmen ihn
beenden (Erreichbarkeit, Isolation, Verfeinerung, verbleibende Angriffsfläche).TrivySupplyChain/layer3/) — das PRISM-MDP/DTMC berechnet
Wahrscheinlichkeiten, erwartete Zeiten und die mehrstufige Kaskade, kalibriert anhand des
OpenSSF-Datensatzes bösartiger Pakete und der dokumentierten Feb→Mär-Zeitleiste.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)
Wo ist
layer2/? Layer 2 (Incident-Rekonstruktion) ist die oberste Ebene vonTrivySupplyChain/— das ModellTrivySupplyChain.tla, die Konfigurationencfg_*.cfg, die ModuleMC*.tla/SecureWorkflow.tlaundrun-all.ps1. Er wurde zuerst als Kern erstellt und liegt daher im Stammverzeichnis;layer1/undlayer3/sind die Validierungsebenen, die darum herum ergänzt wurden.
Voraussetzungen: Windows + ein JDK (JAVA_HOME setzen); Python 3.10+ (Layer 1 und
Kalibrierung); Node.js (nur zum Neuerzeugen der Word-Dokumente); Git für Windows (stellt die
MinGW-Runtime-DLLs bereit, die PRISMs native Bibliothek benötigt). Die TLA+-Werkzeuge und
PRISM sind im Repository gebündelt enthalten.
# 0. verify the toolchain
powershell -File TrivySupplyChain\env-check.ps1
# 1. Layer 2 — all 10 TLC checks (reachability, mitigations, isolation, refinement)
powershell -File TrivySupplyChain\run-all.ps1
# 2. Layer 1 — corpus analysis (unit tests + measured floating-tag fraction)
powershell -File TrivySupplyChain\layer1\run-layer1.ps1
# 3. Layer 3 — PRISM: probabilities, multi-stage cascade, parametric, calibration
powershell -File TrivySupplyChain\layer3\run-layer3.ps1
# 4. (optional) ASI-Evolve mitigation search — Claude Opus proposes policies,
# PRISM verifies each one. Needs the Anthropic SDK + an API key.
pip install -r TrivySupplyChain\asi_evolve\requirements.txt
python TrivySupplyChain\asi_evolve\run_evolve.py
Die Ebenen 1–3 sind in sich abgeschlossen und benötigen keinen API-Schlüssel. Nur der
Vorschlagende in Schritt 4 ist ein LLM; sein PRISM-Orakel (asi_evolve/evaluate.py) läuft
eigenständig und bewertet tatsächlich jede Policy.
Die Quellen .tla, .prism und .py sind portabel; nur die Runner-Skripte sind
Windows-PowerShell. Die manuellen (plattformübergreifenden) Befehle finden Sie in
TrivySupplyChain/README.md.
Layer 3 ist in der gebündelten Form nur für Windows. PRISM wird hier als native Windows-Bibliothek (
prism.dll, CUDD) plus der MinGW-Runtime von Git für Windows ausgeliefert, daher läuftrun-layer3.ps1nur unter Windows. Ein Reviewer unter Linux/macOS kann Layer 3 nicht aus der gebündelten Binärdatei ausführen — die Modelle.prism/.propssind jedoch portabel: Installieren Sie das Upstream-PRISM (https://www.prismmodelchecker.org) und führen Sie sie direkt aus, z. B.prism layer3/trivy_mdp.prism layer3/trivy.props. Die Ebenen 1–2 sind plattformübergreifend (Python, und das gebündeltetla2tools.jarläuft überall mit einem JDK).
📄 Im Browser lesen: main.pdf — GitHub rendert es
inline. Ein direkter Download ist der
v1.0.0-Release
beigefügt.
Trivy-USENIX-paper/main.tex ist die Ausarbeitung im zweispaltigen USENIX-Security-Format.
Sie ist in sich abgeschlossen (Standard-CTAN-Pakete) und kompiliert auf Overleaf oder mit
jeder TeX-Engine:
pdflatex main.tex && pdflatex main.tex # or: tectonic main.tex
Das kompilierte Paper ist main.pdf; der ausgefüllte Validierungsbericht (Word) ist
QA -- Validation Results (Filled In).docx — beide in Trivy-USENIX-paper/.
main — die aktuelle, korrigierte Analyse. Hierauf aufbauen.pre-mercor-fix — eine archivierte Rekonstruktion des Projekts vor der
Umbenennung Mercor→v1 (Mercors Vorfall erfolgte über das LiteLLM-Folgepaket der Stufe 2,
nicht über eine direkte trivy-action-Ausführung). Nur als Referenz; siehe
PRE-MERCOR-FIX.md in diesem Branch.Forschungspreprint in Arbeit von Franklin Hanna (Zugehörigkeit/E-Mail sind in main.tex
weiterhin Platzhalter). Die Fakten zum Vorfall stammen aus dem öffentlichen Dossier (Aqua,
GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV u. a.).
Modellierungsannahmen und ihre Grenzen sind im Abschnitt Einschränkungen und Bedrohungen der
Validität des Papers ausdrücklich dargelegt.
Wenn Sie diese Arbeit verwenden, zitieren Sie bitte die archivierte Veröffentlichung
(Zenodo-DOI 10.5281/zenodo.21387135);
maschinenlesbare Metadaten finden Sie in 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.Gebündelte Drittanbieter-Werkzeuge behalten ihre eigenen Lizenzen: PRISM ist GPL
(TrivySupplyChain/layer3/prism/COPYING.txt), und die TLA+-Werkzeuge sind MIT.