Quantitative Analyse von mehrstufigen CI/CD-Supply-Chain-Angriffen

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.

Was passiert ist und was dies beweist

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:

Vollständige vs. teilweise Rotation von Anmeldedaten. Das Modell beweist, dass die tatsächlich erfolgte teilweise Rotation den Angriff nicht beendet, die vollständige Rotation jedoch schon — was der dokumentierten Incident-Ursache entspricht.
SHA-Pinning isoliert eine Pipeline. Eine auf einen Commit-SHA gepinnte Pipeline ist nachweislich niemals kompromittiert, selbst wenn ihre Nachbarn es sind und selbst wenn die gestohlene Anmeldeinformation gültig bleibt — der Vorfall bleibt auf die nicht gepinnte Teilmenge beschränkt (ein formales Isolationstheorem + eine Verfeinerungsrelation, die die verbleibende Angriffsfläche quantifiziert).
Wie wahrscheinlich, wie schnell, wie weit. Exakte Kompromittierungswahrscheinlichkeiten, erwartete Zeit bis zur Kompromittierung, eine zweistufige npm-Ausbreitungskaskade und Ergebnisse in geschlossener parametrischer Form, kalibriert anhand realer Häufigkeitsdaten bösartiger Pakete.
Das Ergebnis übersteht eine automatisierte Suche. Ein LLM-Vorschlagssystem (Claude Opus 4.8), das den Raum der Verteidiger-Policies gegen das verifizierte PRISM-Orakel durchsucht, konvergiert — ohne menschliche Anleitung — auf dieselbe kostenminimale, nachweislich sichere Policy: Rotation der verbleibenden Anmeldeinformation. Der Vorschlagende schlägt vor; der Modellprüfer entscheidet.

Zentrale Ergebnisse

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

Validierung in drei Ebenen

Strukturelle Wiedergabetreue (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).
Incident-Rekonstruktion (TrivySupplyChain/) — das TLA+-Modell plus 10 TLC-Konfigurationen reproduzieren den Angriff und beweisen, welche Gegenmaßnahmen ihn beenden (Erreichbarkeit, Isolation, Verfeinerung, verbleibende Angriffsfläche).
Prädiktive Kalibrierung (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.

Repository-Struktur

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 von TrivySupplyChain/ — das Modell TrivySupplyChain.tla, die Konfigurationen cfg_*.cfg, die Module MC*.tla / SecureWorkflow.tla und run-all.ps1. Er wurde zuerst als Kern erstellt und liegt daher im Stammverzeichnis; layer1/ und layer3/ sind die Validierungsebenen, die darum herum ergänzt wurden.

Reproduktion

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.

trivysupplychainanalysis

Beliebteste