Analyse quantitative des attaques multi-étapes sur la chaîne d'approvisionnement CI/CD

Une reconstruction quantitative et formellement vérifiée du compromis de la chaîne d'approvisionnement GitHub Actions de Trivy / « TeamPCP » de mars 2026 (CVE-2026-33634) — modélisé en TLA+, vérifié exhaustivement avec TLC, et quantifié avec le vérificateur de modèles probabiliste PRISM.

Chaque nombre de l'article se régénère à partir de ce dépôt. Le modèle, les probabilités, les mesures du corpus et l'étalonnage se reproduisent tous à partir de la source avec une seule commande par couche.

Ce qui s'est passé, et ce que cela prouve

Un attaquant capable de déplacer une balise de version flottante sur une Action largement utilisée (trivy-action / setup-trivy) a fait exécuter à des milliers de pipelines en aval du code contrôlé par l'attaquant avec des identifiants de production lors de leur prochaine exécution de routine, divulguant des secrets qui ont ensemencé un ver npm de deuxième étape. Ce projet pose les questions qu'un rapport d'incident ne peut pas répondre formellement :

• Rotation complète vs. partielle des identifiants. Le modèle prouve que la rotation partielle qui a réellement eu lieu ne ferme pas l'attaque, tandis que la rotation complète le fait — correspondant à la causalité documentée de l'incident.
• L'ancrage SHA isole un pipeline. Un pipeline ancré par SHA de commit n'est jamais compromis de manière prouvable, même lorsque ses voisins le sont et même lorsque l'identifiant volé reste valide — la brèche est contenue au sous-ensemble non ancré (un théorème d'isolation formel + une relation de raffinement quantifiant la surface d'attaque résiduelle).
• Probabilité, rapidité, étendue. Probabilités exactes de compromission, temps attendu jusqu'à compromission, cascade de propagation npm en deux étapes, et résultats paramétriques sous forme fermée, étalonnés par rapport aux données réelles de fréquence des paquets malveillants.
• Le résultat survit à une recherche automatisée. Un proposeur LLM (Claude Opus 4.8) recherchant dans l'espace des politiques de défense par rapport à l'oracle PRISM vérifié converge — sans guidage humain — vers la même politique prouvée sûre à coût minimal : faire tourner l'identifiant résiduel. Le proposeur suggère ; le vérificateur de modèles décide.

Résultats clés

Validation en trois couches

1. Fidélité structurelle (TrivySupplyChain/layer1/) — un analyseur statique sur un corpus de workflows réels GitHub Actions mesure la fréquence d'occurrence des constructions modélisées (14/14 tests unitaires ; la fraction d'étiquettes flottantes alimente la couche 3).
2. Reconstruction de l'incident (TrivySupplyChain/) — le modèle TLA+ + 10 configurations TLC reproduisent l'attaque et prouvent quelles mesures d'atténuation la ferment (atteignabilité, isolation, raffinement, surface résiduelle).
3. Étalonnage prédictif (TrivySupplyChain/layer3/) — le PRISM MDP/DTMC calcule les probabilités, les temps attendus et la cascade multi-étapes, étalonné par rapport au jeu de données OpenSSF des paquets malveillants et à la chronologie documentée Fév→Mar.

Disposition du dépôt

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)

Où se trouve layer2/ ? La couche 2 (reconstruction de l'incident) est le niveau supérieur de TrivySupplyChain/ — le modèle TrivySupplyChain.tla, les configurations cfg_*.cfg, les modules MC*.tla / SecureWorkflow.tla, et run-all.ps1. Elle a été construite en premier comme noyau, donc elle réside à la racine ; layer1/ et layer3/ sont les couches de validation ajoutées autour.

Le reproduire

Prérequis : Windows + un JDK (définir JAVA_HOME) ; Python 3.10+ (Couche 1 & étalonnage) ; Node.js (uniquement pour régénérer les docs Word) ; Git pour Windows (fournit les DLL d'exécution MinGW dont la bibliothèque native de PRISM a besoin). Les outils TLA+ et PRISM sont inclus dans le dépôt.

# 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

Les couches 1 à 3 sont autonomes et ne nécessitent aucune clé API. Seul le proposeur de l'étape 4 est un LLM ; son oracle PRISM (asi_evolve/evaluate.py) fonctionne de manière autonome et est ce qui évalue réellement chaque politique.

Les sources .tla, .prism et .py sont portables ; seuls les scripts d'exécution sont en Windows PowerShell. Voir TrivySupplyChain/README.md pour les commandes manuelles (multi-plateforme).

La couche 3 est exclusivement Windows telle qu'incluse. PRISM est livré ici en tant que bibliothèque Windows native (prism.dll, CUDD) plus l'exécution MinGW de Git pour Windows, donc run-layer3.ps1 ne fonctionne que sur Windows. Un examinateur Linux/macOS ne peut pas exécuter la couche 3 à partir du binaire fourni — mais les modèles .prism/.props sont portables : installez PRISM officiel (https://www.prismmodelchecker.org) et exécutez-les directement, par exemple prism layer3/trivy_mdp.prism layer3/trivy.props. Les couches 1–2 sont multiplateformes (Python, et le tla2tools.jar fourni fonctionne partout avec un JDK).

L'article

📄 Lisez-le dans votre navigateur : main.pdf — GitHub le rend en ligne. Un téléchargement direct est joint à la version v1.0.0.

Trivy-USENIX-paper/main.tex est le manuscrit au format deux colonnes USENIX Security. Il est autonome (paquets CTAN standard) et se compile sur Overleaf ou avec n'importe quel moteur TeX :

pdflatex main.tex && pdflatex main.tex     # or: tectonic main.tex

L'article compilé est main.pdf ; le rapport de validation rempli (Word) est QA -- Validation Results (Filled In).docx — tous deux dans Trivy-USENIX-paper/.

Branches

• main — l'analyse actuelle et corrigée. Construire à partir d'ici.
• pre-mercor-fix — une reconstruction d'archive du projet avant le re-étiquetage Mercor→v1 (la brèche de Mercor est venue via le suivi LiteLLM de l'étape 2, pas d'une exécution directe de trivy-action). Référence uniquement ; voir PRE-MERCOR-FIX.md sur cette branche.

Statut et portée

Préprint de recherche en cours par Franklin Hanna (l'affiliation/l'email sont encore des espaces réservés dans main.tex). Les faits de l'incident sont tirés du dossier public (Aqua, GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV, et autres). Les hypothèses de modélisation et leurs limites sont énoncées explicitement dans la section Limitations and Threats to Validity de l'article.

Citation

Si vous utilisez ce travail, veuillez citer la version archivée (DOI Zenodo 10.5281/zenodo.21387135) ; les métadonnées lisibles par machine se trouvent dans 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}
}

Licence

• Artéfacts de code et méthodes formelles (analyseurs, modèles TLA+/PRISM, scripts, générateurs) — Licence Apache 2.0.
• Texte de l'article et ses versions (Trivy-USENIX-paper/) — CC BY 4.0.

Les outils tiers fournis conservent leurs propres licences : PRISM est GPL (TrivySupplyChain/layer3/prism/COPYING.txt) et les outils TLA+ sont MIT.