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

Validación de tres capas

1. 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).
2. 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).
3. 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.

Los archivos .tla, .prism y .py son portables; solo los scripts de ejecución son PowerShell de Windows. Consulte TrivySupplyChain/README.md para los comandos manuales (multiplataforma).

La Capa 3 es solo para Windows tal como está incluida. PRISM se entrega aquí como su biblioteca nativa de Windows (prism.dll, CUDD) más el runtime MinGW de Git para Windows, por lo que run-layer3.ps1 se ejecuta solo en Windows. Un revisor de Linux/macOS no puede ejecutar la Capa 3 desde el binario incluido — pero los modelos .prism/.props son portables: instale PRISM oficial (https://www.prismmodelchecker.org) y ejecútelos directamente, p. ej. prism layer3/trivy_mdp.prism layer3/trivy.props. Las capas 1–2 son multiplataforma (Python, y el tla2tools.jar incluido se ejecuta en cualquier lugar con un JDK).

El artículo

📄 Léalo en su navegador: main.pdf — GitHub lo renderiza en línea. Una descarga directa está adjunta al lanzamiento v1.0.0.

Trivy-USENIX-paper/main.tex es el documento en formato de dos columnas de USENIX Security. Es autónomo (paquetes CTAN estándar) y compila en Overleaf o con cualquier motor TeX:

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

El artículo compilado es main.pdf; el informe de validación rellenado (Word) es QA -- Validation Results (Filled In).docx — ambos en Trivy-USENIX-paper/.

Ramas

• main — el análisis actual y corregido. Construya desde aquí.
• pre-mercor-fix — una reconstrucción archivada del proyecto antes del reetiquetado de Mercor→v1 (la brecha de Mercor vino a través del seguimiento de LiteLLM en etapa 2, no una ejecución directa de trivy-action). Solo referencia; consulte PRE-MERCOR-FIX.md en esa rama.

Estado y alcance

Preimpresión de investigación en progreso por Franklin Hanna (la afiliación/correo electrónico son todavía marcadores de posición en main.tex). Los hechos del incidente se extraen del expediente público (Aqua, GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV y otros). Los supuestos de modelado y sus límites se exponen explícitamente en la sección Limitaciones y Amenazas a la Validez del artículo.

Citación

Si utiliza este trabajo, cite el lanzamiento archivado (DOI de Zenodo 10.5281/zenodo.21387135); los metadatos legibles por máquina están en 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}
}

Licencia

• Código y artefactos de métodos formales (analizadores, modelos TLA+/PRISM, scripts, generadores) — Licencia Apache 2.0.
• Texto del artículo y sus versiones (Trivy-USENIX-paper/) — CC BY 4.0.

Las herramientas de terceros incluidas mantienen sus propias licencias: PRISM es GPL (TrivySupplyChain/layer3/prism/COPYING.txt) y las herramientas TLA+ son MIT.