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

Validação de três camadas

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

A Camada 3 é apenas Windows como fornecida. O PRISM é enviado aqui como sua biblioteca nativa Windows (prism.dll, CUDD) mais o runtime MinGW do Git para Windows, então run-layer3.ps1 é executado apenas no Windows. Um revisor Linux/macOS não pode executar a Camada 3 a partir do binário fornecido — mas os modelos .prism/.props são portáveis: instale o PRISM oficial (https://www.prismmodelchecker.org) e execute-os diretamente, ex. prism layer3/trivy_mdp.prism layer3/trivy.props. As camadas 1–2 são multiplataforma (Python, e o tla2tools.jar incluído é executado em qualquer lugar com um JDK).

O artigo

📄 Leia no seu navegador: main.pdf — o GitHub renderiza inline. Um download direto está anexado ao lançamento v1.0.0.

Trivy-USENIX-paper/main.tex é o artigo no formato de duas colunas do USENIX Security. Ele é autocontido (pacotes CTAN padrão) e compila no Overleaf ou com qualquer engine TeX:

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

O artigo compilado é main.pdf; o relatório de validação preenchido (Word) é QA -- Validation Results (Filled In).docx — ambos em Trivy-USENIX-paper/.

Ramos

• main — a análise atual e corrigida. Construa a partir daqui.
• pre-mercor-fix — uma reconstrução arquivística do projeto antes da reetiquetagem Mercor→v1 (a violação da Mercor veio através do seguimento LiteLLM de estágio 2, não uma execução direta do trivy-action). Apenas referência; veja PRE-MERCOR-FIX.md nesse ramo.

Status e escopo

Pré-impressão de pesquisa em andamento por Franklin Hanna (afiliação/email ainda são placeholders em main.tex). Os fatos do incidente são extraídos do dossiê público (Aqua, GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV e outros). As suposições de modelagem e seus limites são declarados explicitamente na seção de Limitações e Ameaças à Validade do artigo.

Citação

Se você usar este trabalho, por favor cite o lançamento arquivado (DOI Zenodo 10.5281/zenodo.21387135); os metadados legíveis por máquina estão em 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}
}

Licença

• Código e artefatos de métodos formais (analisadores, modelos TLA+/PRISM, scripts, geradores) — Apache License 2.0.
• Texto do artigo e suas rendições (Trivy-USENIX-paper/) — CC BY 4.0.

Ferramentas de terceiros incluídas mantêm suas próprias licenças: PRISM é GPL (TrivySupplyChain/layer3/prism/COPYING.txt) e as ferramentas TLA+ são MIT.