التحليل الكمّي لهجمات سلسلة التوريد متعددة المراحل في CI/CD

إعادة بناء مُتحقَّق منها شكليًا وكمّية لاختراق سلسلة توريد GitHub Actions المرتبط بـ Trivy / "TeamPCP" في مارس 2026 (CVE-2026-33634) — نُموذجت بلغة TLA+، وفُحصت استنفاديًا باستخدام TLC، وقُدِّرت كمّيًا باستخدام مدقق النماذج الاحتمالي PRISM.

كل رقم في الورقة يُعاد توليده من هذا المستودع. النموذج، والاحتمالات، وقياسات المجموعة النصية، والمعايرة — جميعها قابلة لإعادة الإنتاج من المصدر بأمر واحد لكل طبقة.

ما الذي حدث، وما الذي يُثبته هذا المشروع

مهاجمٌ استطاع تحريك وسم إصدار عائم على Action مستخدمة على نطاق واسع (trivy-action / setup-trivy) تسبّب في أن تنفّذ آلاف خطوط الأنابيب النهائية (downstream) شفرةً يتحكم بها المهاجم مع بيانات اعتماد الإنتاج في تشغيلها الروتيني التالي، مسرّبةً أسرارًا غذّت دودة npm في المرحلة الثانية. يطرح هذا المشروع الأسئلة التي لا يستطيع تقرير الحادثة الإجابة عنها شكليًا:

• التدوير الكامل مقابل التدوير الجزئي لبيانات الاعتماد. يُثبت النموذج أن التدوير الجزئي الذي حدث فعلًا لا يُغلق باب الهجوم، بينما يُغلقه التدوير الكامل — بما يطابق السببية الموثقة للحادثة.
• تثبيت SHA يعزل خط الأنابيب. خط الأنابيب المثبَّت على SHA خاصة بالالتزام (commit-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 قابلة للنقل؛ فقط نصوص التشغيل هي PowerShell الخاصة بـ Windows. راجع TrivySupplyChain/README.md لمعرفة الأوامر اليدوية (المتاحة عبر المنصات).

الطبقة 3 مقتصرة على Windows كما هي مضمّنة. يأتي PRISM هنا كمكتبته الأصلية لنظام Windows (prism.dll، CUDD) بالإضافة إلى بيئة تشغيل MinGW من Git for Windows، لذا يعمل 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 عبر الامتداد اللاحق 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، وغيرهم). افتراضات النمذجة وحدودها مُعلنة صراحةً في قسم القيود وتهديدات الصلاحية من الورقة.

الاستشهاد

إذا استخدمت هذا العمل، فيُرجى الاستشهاد بالإصدار المؤرشف (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.