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

Validazione a tre livelli

1. 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).
2. Ricostruzione dell'incidente (TrivySupplyChain/) — il modello TLA+ + 10 configurazioni TLC riproducono l'attacco e dimostrano quali mitigazioni lo chiudono (raggiungibilità, isolamento, raffinamento, superficie residua).
3. 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

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.

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).

Layer 3 è solo Windows come fornito. PRISM viene qui fornito come sua libreria nativa Windows (prism.dll, CUDD) più il runtime MinGW di Git-for-Windows, quindi run-layer3.ps1 funziona solo su Windows. Un revisore Linux/macOS non può eseguire Layer 3 dal binario fornito — ma i modelli .prism/.props sono portabili: installa il PRISM upstream (https://www.prismmodelchecker.org) ed eseguili direttamente, ad es. prism layer3/trivy_mdp.prism layer3/trivy.props. I Layer 1–2 sono cross-platform (Python, e il tla2tools.jar fornito funziona ovunque con un JDK).

Il paper

📄 Leggilo nel tuo browser: main.pdf — GitHub lo visualizza inline. Un download diretto è allegato alla release v1.0.0.

Trivy-USENIX-paper/main.tex è il documento nel formato a due colonne di USENIX Security. È autonomo (pacchetti CTAN standard) e compila su Overleaf o con qualsiasi motore TeX:

Il paper compilato è main.pdf; il report di validazione compilato (Word) è QA -- Validation Results (Filled In).docx — entrambi in Trivy-USENIX-paper/.

Rami

• main — l'analisi corrente e corretta. Costruisci da qui.
• pre-mercor-fix — una ricostruzione archivistica del progetto prima del rietichettamento Mercor→v1 (la violazione di Mercor è arrivata tramite il follow-on LiteLLM di stadio 2, non una diretta esecuzione di trivy-action). Solo riferimento; vedi PRE-MERCOR-FIX.md su quel ramo.

Stato e ambito

Preprint di ricerca in corso di Franklin Hanna (affiliazione/email sono ancora placeholder in main.tex). I fatti dell'incidente sono tratti dal dossier pubblico (Aqua, GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV e altri). Le ipotesi di modellazione e i loro limiti sono dichiarati esplicitamente nella sezione Limiti e minacce alla validità del paper.

Citazione

Se usi questo lavoro, cita la release archiviata (DOI Zenodo 10.5281/zenodo.21387135); i metadati leggibili da macchina sono in CITATION.cff.

Licenza

• Codice e artefatti di metodi formali (analizzatori, modelli TLA+/PRISM, script, generatori) — Apache License 2.0.
• Testo del paper e sue versioni (Trivy-USENIX-paper/) — CC BY 4.0.

Gli strumenti di terze parti inclusi mantengono le proprie licenze: PRISM è GPL (TrivySupplyChain/layer3/prism/COPYING.txt) e gli strumenti TLA+ sono MIT.