Quantitative Analysis of Multi-Stage CI/CD Supply-Chain Attacks

형식적으로 검증되고 정량적으로 재구성된 2026년 3월 Trivy / "TeamPCP" GitHub Actions 공급망 침해 (CVE-2026-33634) — TLA+로 모델링, TLC로 철저히 확인, PRISM 확률 모델 검사기로 정량화.

논문의 모든 숫자는 이 저장소에서 재생성됩니다. 모델, 확률, 코퍼스 측정값, 보정 모두 레이어당 단일 명령어로 소스에서 재현됩니다.

발생한 일과 이를 통해 입증된 것

널리 사용되는 Action(trivy-action / setup-trivy)의 부동 버전 태그를 옮길 수 있었던 공격자는 수천 개의 하류 파이프라인이 다음 정기 실행 시 프로덕션 자격 증명으로 공격자 제어 코드를 실행하도록 하여, 두 번째 단계 npm 웜을 위한 시드를 유출했습니다. 이 프로젝트는 사고 보고서가 형식적으로 답할 수 없는 질문을 제기합니다:

• 전체 대 부분 자격 증명 교체. 모델은 실제로 발생한 부분 교체가 공격을 차단하지 않는 반면, 전체 교체는 차단함을 증명합니다 — 문서화된 사고 인과 관계와 일치합니다.
• SHA 고정은 파이프라인을 격리합니다. 커밋 SHA 고정 파이프라인은 절대 침해되지 않음이 증명 가능하며, 이웃이 침해되고 유출된 자격 증명이 유효한 상태로 유지되더라도 — 침해는 고정되지 않은 하위 집합으로 제한됩니다 (형식적 격리 정리 + 잔여 공격 표면을 정량화하는 세분화 관계).
• 얼마나 가능성 있고, 얼마나 빠르며, 얼마나 먼지. 정확한 손상 확률, 예상 손상 시간, 2단계 npm 전파 캐스케이드 및 폐쇄형 파라메트릭 결과, 실제 악성 패키지 빈도 데이터에 대해 보정됨.
• 결과는 자동화된 검색에서도 유지됩니다. 방어자 정책 공간을 검색하는 LLM 제안자(Claude Opus 4.8)가 검증된 PRISM 오라클에 대해 수렴합니다 — 인간의 지침 없이 — 동일한 최소 비용 증명 가능 안전 정책: 잔여 자격 증명을 교체하십시오. 제안자가 제안하고; 모델 검사기가 결정합니다.

주요 결과

3층 검증

1. 구조적 충실성 (TrivySupplyChain/layer1/) — 실제 GitHub Actions 워크플로 코퍼스에 대한 정적 분석기로서 모델링된 구조가 얼마나 자주 발생하는지 측정합니다 (14/14 단위 테스트; 부동 태그 비율은 Layer 3에 전달).
2. 사건 재구성 (TrivySupplyChain/) — TLA+ 모델 + 10개의 TLC 구성이 공격을 재현하고 어떤 완화 조치가 이를 차단하는지 증명합니다 (도달 가능성, 격리, 정제, 잔여 표면).
3. 예측 보정 (TrivySupplyChain/layer3/) — PRISM MDP/DTMC가 확률, 예상 시간 및 다단계 캐스케이드를 계산하며, OpenSSF 악성 패키지 데이터셋과 문서화된 2월→3월 타임라인에 대해 보정됩니다.

저장소 구조

TrivySupplyChain/            모델 + 검증 하네스
  TrivySupplyChain.tla       핵심 TLA+ 전이 시스템
  MCTrace.tla, SecureWorkflow.tla, MCRefine.tla
  cfg_*.cfg                  10개의 TLC 구성 (검증 테이블)
  tools/tla2tools.jar        번들된 TLA+ / TLC 2.19
  layer1/                    코퍼스 분석기 (Python) + 픽스처 + 테스트
  layer3/                    PRISM 모델 (.prism/.props) + 번들된 PRISM 4.10.1
  asi_evolve/                LLM 완화 탐색 루프 (run_evolve.py)로 검증된 PRISM 오라클 위에서 + 보관된 실행 결과 (example_run.json)
  run-all.ps1                10개의 TLC 검증 모두 재현
  env-check.ps1              일회성 환경 진단
Trivy-USENIX-paper/          USENIX 논문: main.tex (단독 컴파일), main.pdf,
                             그리고 작성된 검증 결과 .docx
Trivy-TeamPCP-Dossier.md     사건 증적 - 출처가 명시된 증거 기반 (읽기 전용)

layer2/는 어디에 있나요? Layer 2(사건 재구성)는 TrivySupplyChain/의 최상위 단계입니다 — TrivySupplyChain.tla 모델, cfg_*.cfg 구성, MC*.tla / SecureWorkflow.tla 모듈 및 run-all.ps1. 핵심으로 먼저 구축되었으므로 루트에 위치하며, layer1/과 layer3/는 그 주위에 추가된 검증 층입니다.

재현하기

요구 사항: Windows + JDK (JAVA_HOME 설정); Python 3.10+ (Layer 1 및 보정); Node.js (Word 문서 재생성 전용); Git for Windows (PRISM의 네이티브 라이브러리에 필요한 MinGW 런타임 DLL 제공). TLA+ 도구와 PRISM은 저장소에 번들되어 있습니다.

# 0. 도구 체인 확인
powershell -File TrivySupplyChain\env-check.ps1

# 1. Layer 2 — 10개의 TLC 검증 모두 (도달 가능성, 완화, 격리, 정제)
powershell -File TrivySupplyChain\run-all.ps1

# 2. Layer 1 — 코퍼스 분석 (단위 테스트 + 측정된 부동 태그 비율)
powershell -File TrivySupplyChain\layer1\run-layer1.ps1

# 3. Layer 3 — PRISM: 확률, 다단계 캐스케이드, 파라메트릭, 보정
powershell -File TrivySupplyChain\layer3\run-layer3.ps1

# 4. (선택 사항) ASI-Evolve 완화 탐색 — Claude Opus가 정책 제안,
#    PRISM이 각각을 검증. Anthropic SDK + API 키 필요.
pip install -r TrivySupplyChain\asi_evolve\requirements.txt
python TrivySupplyChain\asi_evolve\run_evolve.py

Layer 1~3은 독립적이며 API 키가 필요하지 않습니다. 4단계의 제안자만 LLM이며, PRISM 오라클 (asi_evolve/evaluate.py)은 독립 실행되어 각 정책을 실제로 평가합니다.

.tla, .prism, .py 소스는 이식 가능합니다. 실행기 스크립트만 Windows PowerShell입니다. 수동 (크로스 플랫폼) 명령어는 TrivySupplyChain/README.md를 참조하십시오.

Layer 3은 번들 상태로 Windows 전용입니다. 여기에 PRISM은 네이티브 Windows 라이브러리(prism.dll, CUDD)와 Git-for-Windows MinGW 런타임으로 제공되므로, run-layer3.ps1은 Windows에서만 실행됩니다. Linux/macOS 검토자는 번들된 바이너리에서 Layer 3을 실행할 수 없습니다 — 하지만 .prism/.props 모델은 이식 가능합니다: 업스트림 PRISM(https://www.prismmodelchecker.org)을 설치하고 직접 실행하십시오. 예: prism layer3/trivy_mdp.prism layer3/trivy.props. Layer 1–2는 크로스 플랫폼입니다 (Python, 번들된 tla2tools.jar는 JDK가 있는 모든 곳에서 실행 가능).

논문

📄 브라우저에서 읽기: main.pdf — GitHub에서 인라인 렌더링. 직접 다운로드는 v1.0.0 릴리스에 첨부되어 있습니다.

Trivy-USENIX-paper/main.tex는 USENIX Security 2단 형식의 문서입니다. 자체 포함(표준 CTAN 패키지)되어 있으며 Overleaf 또는 모든 TeX 엔진에서 컴파일됩니다:

pdflatex main.tex && pdflatex main.tex     # 또는: tectonic main.tex

컴파일된 논문은 main.pdf입니다; 작성된 검증 보고서 (Word)는 QA -- Validation Results (Filled In).docx입니다 — 둘 다 Trivy-USENIX-paper/에 있습니다.

브랜치

• main — 현재의 수정된 분석. 여기서 빌드하십시오.
• pre-mercor-fix — Mercor→v1 재명명 이전 프로젝트의 아카이브 재구성 (Mercor의 침해는 직접적인 trivy-action 실행이 아닌 2단계 LiteLLM 후속 공격을 통해 발생). 참고용 전용; 해당 브랜치의 PRE-MERCOR-FIX.md를 참조하십시오.

상태 및 범위

Franklin Hanna의 연구 프리프린트 진행 중 (소속/이메일은 main.tex에서 여전히 플레이스홀더). 사건 사실은 공개 증적 (Aqua, GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV 등)에서 가져왔습니다. 모델링 가정과 한계는 논문의 한계 및 타당성 위협 섹션에 명시되어 있습니다.

인용

이 작업을 사용하는 경우 보관된 릴리스 (Zenodo DOI 10.5281/zenodo.21387135)를 인용해 주십시오; 기계 판독 가능 메타데이터는 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}
}

라이선스

• 코드 및 형식 방법론 아티팩트 (분석기, TLA+/PRISM 모델, 스크립트, 생성기) — Apache License 2.0.
• 논문 텍스트 및 파생물 (Trivy-USENIX-paper/) — CC BY 4.0.

번들된 타사 도구는 자체 라이선스를 유지합니다: PRISM은 GPL (TrivySupplyChain/layer3/prism/COPYING.txt)이며 TLA+ 도구는 MIT입니다.