Количественный анализ многоэтапных атак на цепочку поставок CI/CD

Формально верифицированная количественная реконструкция компрометации цепочки поставок GitHub Actions Trivy / "TeamPCP" в марте 2026 года (CVE-2026-33634) — смоделирована в TLA+, тщательно проверена с помощью TLC и количественно оценена с помощью вероятностного верификатора моделей PRISM.

Каждое число в статье воспроизводится из этого репозитория. Модель, вероятности, измерения корпуса и калибровка — всё воспроизводится из исходного кода одной командой на каждый слой.

Что произошло и что это доказывает

Злоумышленник, способный перемещать плавающий тег версии в широко используемом Action (trivy-action / setup-trivy), вызвал выполнение управляемого злоумышленником кода с производственными учетными данными в тысячах нижестоящих конвейеров при их следующем плановом запуске, что привело к утечке секретов, которые послужили основой для npm-червя второй стадии. Этот проект задает вопросы, на которые отчет об инциденте не может ответить формально:

• Полная и частичная ротация учетных данных. Модель доказывает, что частичная ротация, которая фактически произошла, не закрывает атаку, в то время как полная ротация — закрывает, что соответствует задокументированной причинно-следственной связи инцидента.
• Фиксация SHA изолирует конвейер. Конвейер с фиксацией по SHA коммита доказуемо никогда не бывает скомпрометирован, даже если его соседи скомпрометированы и даже если украденные учетные данные остаются действительными — нарушение ограничивается незакрепленным подмножеством (формальная теорема изоляции + отношение уточнения, количественно оценивающее остаточную поверхность атаки).
• Насколько вероятно, как быстро, как далеко. Точные вероятности компрометации, ожидаемое время до компрометации, двухэтапный каскад распространения npm и параметрические результаты в замкнутой форме, откалиброванные по реальным данным о частоте вредоносных пакетов.
• Результат выдерживает автоматический поиск. Предлагатель LLM (Claude Opus 4.8), выполняющий поиск в пространстве политик защиты с проверенным оракулом PRISM, сходится — без участия человека — к той же политике с минимальной стоимостью, доказуемо безопасной: ротация оставшихся учетных данных. Предлагатель предлагает; верификатор моделей решает.

Ключевые результаты

Трехслойная валидация

1. Структурная точность (TrivySupplyChain/layer1/) — статический анализатор, работающий с корпусом реальных рабочих процессов GitHub Actions, измеряет, как часто встречаются моделируемые конструкции (14/14 модульных тестов; доля плавающих тегов поступает в Слой 3).
2. Реконструкция инцидента (TrivySupplyChain/) — модель TLA+ + 10 конфигураций TLC воспроизводят атаку и доказывают, какие смягчающие меры её закрывают (достижимость, изоляция, уточнение, остаточная поверхность).
3. Прогностическая калибровка (TrivySupplyChain/layer3/) — PRISM MDP/DTMC вычисляет вероятности, ожидаемое время и многоэтапный каскад, откалиброванные по набору данных OpenSSF о вредоносных пакетах и задокументированной временной шкале Февраль→Март.

Структура репозитория

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)

Где layer2/? Слой 2 (реконструкция инцидента) является верхним уровнем TrivySupplyChain/ — модель TrivySupplyChain.tla, конфиги cfg_*.cfg, модули MC*.tla / SecureWorkflow.tla и run-all.ps1. Он был создан первым как ядро, поэтому находится в корне; layer1/ и layer3/ — это слои валидации, добавленные вокруг.

Воспроизведение

Требования: Windows + JDK (установите JAVA_HOME); Python 3.10+ (Слой 1 и калибровка); Node.js (только для регенерации документов Word); Git for Windows (предоставляет библиотеки времени выполнения MinGW, необходимые нативной библиотеке PRISM). Инструменты TLA+ и PRISM включены в репозиторий.

# 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

Слои 1–3 являются самодостаточными и не требуют ключа API. Только предлагатель шага 4 является LLM; его оракул PRISM (asi_evolve/evaluate.py) работает автономно и фактически оценивает каждую политику.

Исходные файлы .tla, .prism и .py переносимы; только скрипты запуска являются Windows PowerShell. См. TrivySupplyChain/README.md для ручных (кроссплатформенных) команд.

Слой 3 работает только на Windows в собранном виде. PRISM поставляется здесь как нативная библиотека Windows (prism.dll, CUDD) плюс среда выполнения Git-for-Windows MinGW, поэтому run-layer3.ps1 работает только на Windows. Рецензент на Linux/macOS не может запустить Слой 3 из встроенного бинарника — но модели .prism/.props переносимы: установите upstream PRISM (https://www.prismmodelchecker.org) и запускайте их напрямую, например prism layer3/trivy_mdp.prism layer3/trivy.props. Слои 1–2 кроссплатформенны (Python, а встроенный tla2tools.jar работает везде, где есть JDK).

Статья

📄 Читайте в браузере: main.pdf — GitHub отображает его встроенно. Прямая загрузка прикреплена к релизу v1.0.0.

Trivy-USENIX-paper/main.tex — это описание в двухколоночном формате USENIX Security. Он самодостаточен (стандартные пакеты CTAN) и компилируется на Overleaf или с любым TeX-движком:

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

Скомпилированная статья — main.pdf; заполненный отчет о валидации (Word) — QA -- Validation Results (Filled In).docx — оба в Trivy-USENIX-paper/.

Ветки

• main — текущий исправленный анализ. Сборка отсюда.
• pre-mercor-fix — архивная реконструкция проекта до переименования Mercor→v1 (нарушение Mercor произошло через продолжение LiteLLM на этапе 2, а не прямое выполнение trivy-action). Только для справки; см. 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.