Количественный анализ многоэтапных атак на цепочку поставок 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, сходится — без участия человека — к той же политике с минимальной стоимостью, доказуемо безопасной: ротация оставшихся учетных данных. Предлагатель предлагает; верификатор моделей решает.

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

Вопрос	Результат
Достижима ли задокументированная атака?	Да — TLC возвращает точный 3-шаговый след из досье
Достаточна ли частичная ротация?	Нет (проверка `NoExfiltration` не проходит); полная ротация да
Фиксация SHA в смешанной популяции	Изоляция выполняется для 8 185 состояний; нарушение локализовано
P(компрометация), уязвимая конфигурация	1.0; E[время] 6 дней; P(≤30 дней) 0.9985
Многоэтапный каскад	P(достижение этапа 2) = q; E[первый нижестоящий] 16 дней; ротация → 0
Параметрический (замкнутая форма)	E[дни до компрометации] = (p+1)/p; P(этап 2) = q (точно)
Корпус слоя 1 (189 реальных рабочих процессов)	доля плавающих тегов f = 0.3698; покрытие конструкций 88.2%
Калибровка (OpenSSF/OSV)	npm = 214 497 отчетов (94.2%); Февраль→Март 2026: 329 → 1,048 (×3.19)
Автоматический поиск смягчающих мер	LLM предлагает, PRISM проверяет → оптимум только ротация (оценка −0.05), сходимость за 4 раунда

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

Структурная точность (TrivySupplyChain/layer1/) — статический анализатор, работающий с корпусом реальных рабочих процессов GitHub Actions, измеряет, как часто встречаются моделируемые конструкции (14/14 модульных тестов; доля плавающих тегов поступает в Слой 3).
Реконструкция инцидента (TrivySupplyChain/) — модель TLA+ + 10 конфигураций TLC воспроизводят атаку и доказывают, какие смягчающие меры её закрывают (достижимость, изоляция, уточнение, остаточная поверхность).
Прогностическая калибровка (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 для ручных (кроссплатформенных) команд.

trivysupplychainanalysis

Популярное