मल्टी-स्टेज CI/CD सप्लाई-चेन हमलों का मात्रात्मक विश्लेषण

मार्च-2026 के Trivy / "TeamPCP" GitHub Actions सप्लाई-चेन समझौते (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 रनटाइम DLL प्रदान करता है जो 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 मॉडल पोर्टेबल हैं: अपस्ट्रीम 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 का उल्लंघन चरण-2 LiteLLM अनुवर्ती के माध्यम से आया था, प्रत्यक्ष trivy-action निष्पादन से नहीं)। केवल संदर्भ; उस शाखा पर PRE-MERCOR-FIX.md देखें।

स्थिति और दायरा

Franklin Hanna द्वारा प्रगति पर शोध प्रीप्रिंट (संबद्धता/ईमेल अभी भी main.tex में प्लेसहोल्डर हैं)। घटना के तथ्य सार्वजनिक डोजियर (Aqua, GHSA, CVE-2026-33634, Unit 42, Microsoft, Wiz, ReversingLabs, Endor Labs, OpenSSF/OSV, और अन्य) से लिए गए हैं। मॉडलिंग धारणाएँ और उनकी सीमाएँ पेपर के Limitations and Threats to Validity खंड में स्पष्ट रूप से बताई गई हैं।

उद्धरण

यदि आप इस कार्य का उपयोग करते हैं, तो कृपया संग्रहीत रिलीज़ (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 हैं।