Análisis Cuantitativo de Ataques a la Cadena de Suministro CI/CD de Múltiples Etapas

Una reconstrucción cuantitativa y formalmente verificada del compromiso de la cadena de suministro de GitHub Actions de Trivy / "TeamPCP" de marzo de 2026 (CVE-2026-33634) — modelado en TLA+, verificado exhaustivamente con TLC, y cuantificado con el verificador de modelos probabilísticos PRISM.

Cada número en el artículo se regenera desde este repositorio. El modelo, las probabilidades, las mediciones del corpus y la calibración se reproducen desde la fuente con un solo comando por capa.

Qué sucedió y qué demuestra esto

Un atacante que pudo mover una etiqueta de versión flotante en una Acción ampliamente utilizada (trivy-action / setup-trivy) provocó que miles de pipelines posteriores ejecutaran código controlado por el atacante con credenciales de producción en su próxima ejecución rutinaria, filtrando secretos que sembraron un gusano npm de segunda etapa. Este proyecto hace las preguntas que un informe de incidente no puede responder formalmente:

Rotación completa vs. parcial de credenciales. El modelo demuestra que la rotación parcial que realmente ocurrió no cierra el ataque, mientras que la rotación completa sí lo hace, coincidiendo con la causalidad documentada del incidente.
El anclaje SHA aísla un pipeline. Un pipeline anclado a un commit-SHA está demostrablemente nunca comprometido, incluso cuando sus vecinos lo están e incluso cuando la credencial robada sigue siendo válida — la brecha se contiene al subconjunto no anclado (un teorema de aislamiento formal + una relación de refinamiento que cuantifica la superficie de ataque residual).
Qué tan probable, qué tan rápido, qué tan lejos. Probabilidades exactas de compromiso, tiempo esperado hasta el compromiso, una cascada de propagación npm de dos etapas y resultados paramétricos de forma cerrada, calibrados con datos reales de frecuencia de paquetes maliciosos.
El hallazgo sobrevive a una búsqueda automatizada. Un proponente LLM (Claude Opus 4.8) que busca el espacio de políticas del defensor contra el oráculo PRISM verificado converge — sin guía humana — en la misma política comprobadamente segura de costo mínimo: rotar la credencial residual. El proponente sugiere; el verificador de modelos decide.

Resultados clave

Pregunta	Resultado
¿Es alcanzable el ataque documentado?	Sí — TLC devuelve el rastro exacto del expediente de 3 pasos
¿Es suficiente la rotación parcial?	No (`NoExfiltration` falla); la rotación completa sí
Anclaje SHA en una población mixta	El aislamiento se mantiene sobre 8,185 estados; la brecha contenida
P(compromiso), config vulnerable	1.0; E[tiempo] 6 días; P(≤30 días) 0.9985
Cascada de múltiples etapas	P(alcanzar etapa 2) = q; E[primer downstream] 16 días; rotación → 0
Paramétrico (forma cerrada)	E[días-hasta-compromiso] = (p+1)/p; P(etapa 2) = q (exacto)
Corpus de capa 1 (189 flujos de trabajo reales)	fracción de etiqueta flotante f = 0.3698; cobertura de constructos 88.2%
Calibración (OpenSSF/OSV)	npm = 214,497 informes (94.2%); Feb→Mar 2026: 329 → 1,048 (×3.19)
Búsqueda automatizada de mitigación	LLM propone, PRISM verifica → óptimo de solo rotación (puntuación −0.05), convergió en 4 rondas

Validación de tres capas

Fidelidad estructural (TrivySupplyChain/layer1/) — un analizador estático sobre un corpus de flujos de trabajo reales de GitHub Actions mide la frecuencia con la que ocurren los constructos modelados (14/14 pruebas unitarias; la fracción de etiqueta flotante alimenta la Capa 3).
Reconstrucción del incidente (TrivySupplyChain/) — el modelo TLA+ + 10 configuraciones TLC reproducen el ataque y demuestran qué mitigaciones lo cierran (accesibilidad, aislamiento, refinamiento, superficie residual).
Calibración predictiva (TrivySupplyChain/layer3/) — el MDP/DTMC de PRISM calcula probabilidades, tiempos esperados y la cascada de múltiples etapas, calibrados con el conjunto de datos de paquetes maliciosos de OpenSSF y la línea de tiempo documentada de febrero a marzo.

Estructura del repositorio

TrivySupplyChain/            El modelo + el entorno de verificación
  TrivySupplyChain.tla       Sistema de transición TLA+ central
  MCTrace.tla, SecureWorkflow.tla, MCRefine.tla
  cfg_*.cfg                  10 configuraciones TLC (la tabla de validación)
  tools/tla2tools.jar        TLA+ / TLC 2.19 incluido
  layer1/                    Analizador de corpus (Python) + fixtures + pruebas
  layer3/                    Modelos PRISM (.prism/.props) + PRISM 4.10.1 incluido
  asi_evolve/                Bucle de búsqueda de mitigación LLM (run_evolve.py) sobre el
                             oráculo PRISM verificado + una ejecución archivada (example_run.json)
  run-all.ps1                Reproduce las 10 comprobaciones TLC
  env-check.ps1              Diagnóstico rápido del entorno
Trivy-USENIX-paper/          Artículo USENIX: main.tex (compila de forma independiente), main.pdf,
                             y el informe de resultados de validación rellenado .docx
Trivy-TeamPCP-Dossier.md     Expediente del incidente — la base de evidencia documentada (solo lectura)

¿Dónde está layer2/? La Capa 2 (reconstrucción del incidente) es el nivel superior de TrivySupplyChain/ — el modelo TrivySupplyChain.tla, las configuraciones cfg_*.cfg, los módulos MC*.tla / SecureWorkflow.tla y run-all.ps1. Se construyó primero como el núcleo, por lo que reside en la raíz; layer1/ y layer3/ son las capas de validación añadidas a su alrededor.

Reproducirlo

Requisitos: Windows + un JDK (establecer JAVA_HOME); Python 3.10+ (Capa 1 y calibración); Node.js (solo para regenerar los documentos Word); Git para Windows (proporciona las DLL del runtime MinGW que necesita la biblioteca nativa de PRISM). Las herramientas TLA+ y PRISM están incluidas en el repositorio.

# 0. verificar la cadena de herramientas
powershell -File TrivySupplyChain\env-check.ps1

# 1. Capa 2 — las 10 comprobaciones TLC (accesibilidad, mitigaciones, aislamiento, refinamiento)
powershell -File TrivySupplyChain\run-all.ps1

# 2. Capa 1 — análisis del corpus (pruebas unitarias + fracción de etiqueta flotante medida)
powershell -File TrivySupplyChain\layer1\run-layer1.ps1

# 3. Capa 3 — PRISM: probabilidades, cascada de múltiples etapas, paramétrico, calibración
powershell -File TrivySupplyChain\layer3\run-layer3.ps1

# 4. (opcional) Búsqueda de mitigación ASI-Evolve — Claude Opus propone políticas,
#    PRISM verifica cada una. Necesita el SDK de Anthropic + una clave API.
pip install -r TrivySupplyChain\asi_evolve\requirements.txt
python TrivySupplyChain\asi_evolve\run_evolve.py

Las capas 1–3 son autónomas y no necesitan clave API. Solo el proponente del paso 4 es un LLM; su oráculo PRISM (asi_evolve/evaluate.py) se ejecuta de forma independiente y es lo que realmente puntúa cada política.

trivysupplychainanalysis

Más Populares