Análise Quantitativa de Ataques à Cadeia de Suprimentos CI/CD de Múltiplos Estágios

Uma reconstrução quantitativa formalmente verificada do comprometimento da cadeia de suprimentos do GitHub Actions Trivy / "TeamPCP" de março de 2026 (CVE-2026-33634) — modelada em TLA+, verificada exaustivamente com TLC e quantificada com o verificador de modelos probabilísticos PRISM.

Cada número no artigo é regenerado a partir deste repositório. O modelo, as probabilidades, as medições do corpus e a calibragem são todos reproduzidos a partir da fonte com um único comando por camada.

O que aconteceu e o que isso prova

Um atacante que conseguiu mover uma tag de versão flutuante em uma Action amplamente utilizada (trivy-action / setup-trivy) fez com que milhares de pipelines downstream executassem código controlado pelo atacante com credenciais de produção em sua próxima execução de rotina, vazando segredos que semearam um worm npm de segundo estágio. Este projeto faz as perguntas que um relatório de incidente não pode responder formalmente:

Rotação completa vs. parcial de credenciais. O modelo prova que a rotação parcial que realmente ocorreu não fecha o ataque, enquanto a rotação completa fecha — correspondendo à causalidade documentada do incidente.
O pinning de SHA isola um pipeline. Um pipeline com pinning de SHA de commit é comprovadamente nunca comprometido, mesmo quando seus vizinhos estão e mesmo quando a credencial roubada permanece válida — a violação é contida ao subconjunto sem pinning (um teorema de isolamento formal + uma relação de refinamento que quantifica a superfície de ataque residual).
Qual a probabilidade, quão rápido, quão longe. Probabilidades exatas de comprometimento, tempo esperado para comprometimento, uma cascata de propagação npm de dois estágios e resultados paramétricos de forma fechada, calibrados com dados reais de frequência de pacotes maliciosos.
A descoberta sobrevive a uma busca automatizada. Um proponente LLM (Claude Opus 4.8) pesquisando o espaço de políticas de defesa contra o oráculo verificado do PRISM converge — sem orientação humana — para a mesma política de custo mínimo comprovadamente segura: rotacione a credencial residual. O proponente sugere; o verificador de modelos decide.

Resultados principais

Pergunta	Resultado
O ataque documentado é alcançável?	Sim — TLC retorna o rastro exato do dossiê de 3 passos
Rotação parcial suficiente?	Não (`NoExfiltration` falha); rotação completa sim
Pinning de SHA em uma população mista	Isolamento mantém-se em 8.185 estados; violação contida
P(comprometimento), configuração vulnerável	1.0; E[tempo] 6 dias; P(≤30 dias) 0.9985
Cascata de múltiplos estágios	P(atingir estágio 2) = q; E[primeiro downstream] 16 dias; rotação → 0
Paramétrico (forma fechada)	E[dias-para-comprometimento] = (p+1)/p; P(estágio 2) = q (exato)
Camada-1 corpus (189 workflows reais)	fração de tag flutuante f = 0.3698; cobertura de construção 88.2%
Calibragem (OpenSSF/OSV)	npm = 214.497 reports (94.2%); Feb→Mar 2026: 329 → 1.048 (×3.19)
Busca automatizada de mitigação	LLM propõe, PRISM verifica → ótimo apenas-rotação (score −0.05), convergido em 4 rodadas

Validação de três camadas

Fidelidade estrutural (TrivySupplyChain/layer1/) — um analisador estático sobre um corpus de workflows reais do GitHub Actions mede com que frequência as construções modeladas ocorrem (14/14 testes unitários; a fração de tag flutuante alimenta a Camada 3).
Reconstrução do incidente (TrivySupplyChain/) — o modelo TLA+ + 10 configurações do TLC reproduzem o ataque e provam quais mitigações o fecham (alcançabilidade, isolamento, refinamento, superfície residual).
Calibragem preditiva (TrivySupplyChain/layer3/) — o MDP/DTMC do PRISM calcula probabilidades, tempos esperados e a cascata de múltiplos estágios, calibrados contra o conjunto de dados de pacotes maliciosos do OpenSSF e a linha do tempo documentada de fevereiro a março (Feb→Mar).

Layout do repositório

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)

Onde está layer2/? A Camada 2 (reconstrução do incidente) é o nível superior de TrivySupplyChain/ — o modelo TrivySupplyChain.tla, as configurações cfg_*.cfg, os módulos MC*.tla / SecureWorkflow.tla e run-all.ps1. Foi construída primeiro como o núcleo, então reside na raiz; layer1/ e layer3/ são as camadas de validação adicionadas ao redor.

Reproduza

Requisitos: Windows + um JDK (defina JAVA_HOME); Python 3.10+ (Camada 1 e calibragem); Node.js (apenas para regenerar os documentos Word); Git para Windows (fornece as DLLs de runtime MinGW que a biblioteca nativa do PRISM precisa). As ferramentas TLA+ e o PRISM estão incluídos no repositório.

# 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

As camadas 1–3 são autocontidas e não precisam de chave de API. Apenas o proponente do passo 4 é um LLM; seu oráculo PRISM (asi_evolve/evaluate.py) é executado de forma independente e é o que realmente pontua cada política.

Os fontes .tla, .prism e .py são portáveis; apenas os scripts de execução são Windows PowerShell. Veja TrivySupplyChain/README.md para os comandos manuais (multiplataforma).

trivysupplychainanalysis

Mais Populares