Analisi Quantitativa degli Attacchi alla Supply-Chain CI/CD Multi-Stadio

Una ricostruzione quantitativa e formalmente verificata del compromesso della supply-chain di GitHub Actions Trivy / "TeamPCP" del marzo 2026 (CVE-2026-33634) — modellata in TLA+, controllata esaustivamente con TLC e quantificata con il model checker probabilistico PRISM.

Ogni numero nel paper si rigenera da questo repository. Il modello, le probabilità, le misurazioni del corpus e la calibrazione si riproducono tutti dal sorgente con un singolo comando per livello.

Cosa è successo e cosa dimostra questo

Un attaccante in grado di spostare un tag di versione fluttuante su un'Action molto utilizzata (trivy-action / setup-trivy) ha causato migliaia di pipeline downstream ad eseguire codice controllato dall'attaccante con credenziali di produzione al loro prossimo esecuzione di routine, facendo trapelare segreti che hanno seminato un worm npm di secondo stadio. Questo progetto si pone le domande a cui un rapporto di incidente non può rispondere formalmente:

Rotazione completa vs. parziale delle credenziali. Il modello dimostra che la rotazione parziale che è effettivamente avvenuta non chiude l'attacco, mentre la rotazione completa lo fa — corrispondendo alla causalità documentata dell'incidente.
Lo SHA-pinning isola una pipeline. Una pipeline ancorata a un commit-SHA non è mai compromessa, anche quando i suoi vicini lo sono e anche quando la credenziale rubata rimane valida — la violazione è contenuta nel sottoinsieme non ancorato (un teorema formale di isolamento + una relazione di raffinamento che quantifica la superficie d'attacco residua).
Quanto probabile, quanto veloce, quanto lontano. Probabilità di compromissione esatte, tempo previsto per la compromissione, una cascata di propagazione npm a due stadi e risultati parametrici in forma chiusa, calibrati su dati reali di frequenza di pacchetti malevoli.
Il risultato sopravvive a una ricerca automatizzata. Un propositore LLM (Claude Opus 4.8) che esplora lo spazio delle politiche del difensore contro l'oracolo PRISM verificato converge — senza guida umana — sulla stessa politica a costo minimo provabilmente sicura: ruotare la credenziale residua. Il propositore suggerisce; il model checker decide.

Risultati chiave

Domanda	Risultato
L'attacco documentato è raggiungibile?	Sì — TLC restituisce la traccia esatta del dossier in 3 passaggi
La rotazione parziale è sufficiente?	No (`NoExfiltration` fallisce); la rotazione completa sì
SHA-pinning in una popolazione mista	L'isolamento vale su 8.185 stati; violazione contenuta
P(compromissione), configurazione vulnerabile	1.0; E[tempo] 6 giorni; P(≤30 giorni) 0.9985
Cascata multi-stadio	P(raggiunge stadio 2) = q; E[primo downstream] 16 giorni; rotazione → 0
Parametrico (forma chiusa)	E[giorni-alla-compromissione] = (p+1)/p; P(stadio 2) = q (esatto)
Corpus Layer-1 (189 workflow reali)	frazione di tag fluttuante f = 0.3698; copertura del costrutto 88.2%
Calibrazione (OpenSSF/OSV)	npm = 214.497 report (94.2%); Feb→Mar 2026: 329 → 1.048 (×3.19)
Ricerca automatizzata di mitigazione	LLM propone, PRISM verifica → ottimo solo rotazione (punteggio −0.05), convergente in 4 round

Validazione a tre livelli

Fedeltà strutturale (TrivySupplyChain/layer1/) — un analizzatore statico su un corpus di workflow reali di GitHub Actions misura quanto spesso si verificano i costrutti modellati (14/14 test unitari; la frazione di tag fluttuante alimenta Layer 3).
Ricostruzione dell'incidente (TrivySupplyChain/) — il modello TLA+ + 10 configurazioni TLC riproducono l'attacco e dimostrano quali mitigazioni lo chiudono (raggiungibilità, isolamento, raffinamento, superficie residua).
Calibrazione predittiva (TrivySupplyChain/layer3/) — il PRISM MDP/DTMC calcola probabilità, tempi previsti e la cascata multi-stadio, calibrati sul dataset di pacchetti malevoli OpenSSF e sulla cronologia documentata Feb→Mar.

Struttura del repository

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)

Dov'è layer2/? Il Layer 2 (ricostruzione dell'incidente) è il livello superiore di TrivySupplyChain/ — il modello TrivySupplyChain.tla, le configurazioni cfg_*.cfg, i moduli MC*.tla / SecureWorkflow.tla e run-all.ps1. È stato costruito per primo come nucleo, quindi si trova nella radice; layer1/ e layer3/ sono i livelli di validazione aggiunti attorno.

Riproducilo

Requisiti: Windows + un JDK (imposta JAVA_HOME); Python 3.10+ (Layer 1 e calibrazione); Node.js (solo per rigenerare i documenti Word); Git per Windows (fornisce le DLL runtime MinGW necessarie per la libreria nativa di PRISM). Gli strumenti TLA+ e PRISM sono inclusi nel repository.

# 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

I Layer 1–3 sono autonomi e non necessitano di chiave API. Solo il propositore del passo 4 è un LLM; il suo oracolo PRISM (asi_evolve/evaluate.py) funziona in modo indipendente ed è ciò che effettivamente valuta ogni politica.

I sorgenti .tla, .prism e .py sono portabili; solo gli script di esecuzione sono Windows PowerShell. Vedi TrivySupplyChain/README.md per i comandi manuali (cross-platform).

trivysupplychainanalysis

Più Popolari