Maude-HCS

Maude-HCS هي واحدة من أولى سلاسل الأدوات المعممة والمعيارية لتحديد النماذج الرسمية والاستدلال حول أنظمة الاتصالات المخفية (HCS) على نطاق العالم الحقيقي. فهي تتيح لمصممي الشبكات استكشاف تصاميم بديلة لأنظمة HCS بسرعة وفعالية وتوفر ضمانات رسمية للخصوصية والأداء اللازمة للوثوق بالتصميم.

مقدمة

أنظمة الاتصالات المخفية (HCS) تضمّن رسائل سرية داخل نشاط الشبكة العادي لإخفاء وجود الاتصال. في الممارسة العملية، يتم عادةً تقييم عدم قابلية كشف نظام HCS باستخدام إحصائيات مرورية مخصصة أو كاشفات محددة، مما يجعل ادعاءات الأمان مرتبطة ارتباطًا وثيقًا بالإعدادات التجريبية والافتراضات الخصومية الضمنية.

Maude-HCS هو إطار عمل للنمذجة والتحليل قابل للتنفيذ يوفر أساسًا مبدئيًا وقابلًا للتنفيذ للاستدلال حول مفاضلات عدم القابلية للكشف مقابل الأداء في تصاميم HCS المعقدة. يحدد المصممون رسميًا سلوك البروتوكول، والملاحظات المتاحة للخصم، والافتراضات البيئية، ويولدون عينات مونت كارلو من التوزيعات الأثرية المستنبطة. يمكن استخدام هذه العينات لمراجعة ادعاءات عدم الكشف من خلال تقدير معدلات الإيجابية الحقيقية والخاطئة لاختبار إحصائي وتحويل هذه التقديرات إلى حدود دنيا لمقاييس عدم الكشف. وهذا يتيح التقييم المنهجي لقابلية الكشف ومقايضاتها مع الأداء تحت افتراضات نمذجة معلنة صراحةً.

يرجى التواصل معنا إذا كنت بحاجة إلى مساعدة في نمذجة والاستدلال حول نظام HCS الخاص بك. ونرجو النظر في الاستشهاد بعملنا إذا استخدمته كجزء من بحثك.```bibtex @article{khoury2026maude, title={Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems}, author={Khoury, Joud and Kim, Minyoung and Merlin, Christophe and Meseguer, Jos{'e} and Ratliff, Zachary and Talcott, Carolyn}, journal={arXiv preprint arXiv:2603.03369}, year={2026} }

## المتطلبات
يتطلب إصدار بايثون `3.12.4`

قم بإنشاء البيئة المفضلة لديك وقم بتفعيلها، على سبيل المثال

لـ pyenv```bash
pyenv install 3.12.4
pyenv local 3.12.4

لـ conda```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2

للبيئة الافتراضية```bash
python -m venv venv
source venv/bin/activate

التثبيت: من مصدر git

لقد قمنا بتنظيم شفرة مصدر المستودع بحيث نقوم باستيراد dns-formalization-maude كاعتمادية (وحدة فرعية). لقد قمنا بإنشاء فرع لهذه الاعتمادية حتى نتمكن من تتبع تغييراتنا عليها. نستخدم sparse-checkout لتجنب الحاجة إلى سحب كل مصدر الاعتمادية الذي يتضمن العديد من الملفات غير ذات الصلة (مثل Testbed).

لاستنساخ المستودع الرئيسي```shell git clone [email protected]:raytheonbbn/maude-hcs.git

الفرع الرئيسي يحتوي على أحدث مصدر (ربما غير مستقر).
الفروع/العلامات الأقدم مثل `pwnd.cp1` تشير إلى لقطات مستقرة استُخدمت لإنتاج نتائج أثناء التقييمات 
(على سبيل المثال، استُخدم `pwnd.cp1` لمشكلة التحدي 1، وبالمثل `pwnd.cp2`).
لاستخدام لقطة أقدم، قم بتسجيل الخروج من الفرع المحدد (مثل `pwnd.cp1`).

قم بإعداد الوحدة الفرعية dns باستخدام نسختنا من الكود حتى نتمكن من تتبع التغييرات 
التي تم إجراؤها على المصدر الأصلي، استخدم sparse-checkout للحفاظ على المصادر ذات الصلة فقط```shell
cd maude-hcs
mkdir -p maude_hcs/deps
git submodule add -b <branch> -f [email protected]:raytheonbbn/dns-formalization-maude.git \
  maude_hcs/deps/dns_formalization
cd maude_hcs/deps/dns_formalization
git sparse-checkout init --cone
git sparse-checkout set "Maude/dns" "Maude/common" "Maude/test" "Maude/attack_exploration"
cd ../../../
git reset .gitmodules
git reset maude_hcs/deps/dns_formalization

في الأمر أعلاه، قم بتعيين <branch> إما إلى pwnd.43.rb1 لإعادة إنتاج نتائج تحدي المشكلة 1، أو إلى pwnd للحصول على أحدث إصدار.

يجب أن يؤدي ما سبق إلى إنشاء ملف جديد باسم sparse-checkout تحت
.git/modules/maude_hcs/deps/dns_formalization/info/
وتوجيهه ليشمل فقط أدلة معينة مثل Maude/src.

عند هذه النقطة، يجب أن يُظهر git status بداية نظيفة.

للتثبيت، قم أولاً بتثبيت التبعية كحزمة تُسمى dns، ونستوردها بصيغة Maude.*
ثم قم بتثبيت maude_hcs كحزمة (مع تبعية على dns).```shell cd maude_hcs/deps/dns_formalization pip install -e . cd ../../../ pip install -e .

## إنشاء نماذج المستخدم تلقائياً

نماذج المستخدم هي نماذج ماركوف (Markov) تهدف إلى تمثيل كيفية تصرف المستخدمين.
يتم تقديم هذه النماذج بصيغة JSON.
الخطوة الأولى هي تحويل هذه النماذج إلى تمثيلات Maude الرسمية.

للقيام بذلك، حدد
 - البروتوكول: dns أو mastodon
 - دليل الإدخال الذي يحتوي على جميع نماذج JSON التي تريد تحويلها
 - دليل الإخراج الذي سيحتوي على جميع إصدارات Maude لنماذج JSON

على سبيل المثال،```shell
# convert dns tgen user models
 maude-hcs --verbose \ 
    --protocol=dns markov \
    --json-dir=../pwnd-cp2/src/static/tgen_models/dns/ \ 
    --maude-dir=./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
    
# convert mastodon tgen models
maude-hcs --verbose \
    --protocol=mastodon markov \
    --json-dir=../pwnd-cp2/src/static/tgen_models/mastodon \
    --maude-dir="./maude_hcs/lib/raceboat/maude/mastodonprofiles/"

شاهد أمثلة على مواصفات ماركوف بصيغة JSON تحت ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/ (وبالمثل بالنسبة لماستودون)، بالإضافة إلى مواصفاتها المحولة إلى Maude.

إنشاء تكوينات HCS تلقائيًا

نقوم بإنشاء التكوينات الأولية باستخدام الأمر generate. يمكن تمرير تكوينات HCS مباشرة بصيغة JSON باستخدام معلمات تكوين HCS، أو باستخدام ملف تكوين تجربة Shadow، أو باستخدام ملف تكوين YML. كل من هذه الطرق موصوفة فيما يلي.

استخدام تكوين HCS بصيغة JSON

مرر ملف تكوين maude-hcs بصيغة JSON كالتالي،

لتوليد نموذج DNS احتمالي باستخدام iodine وتحديد اسم ملف الإخراج،```shell maude-hcs --verbose generate
--run-args="./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1-hcsconfig.json"
--model=prob
--filename="cp2_scenario_1"
--output-dir="./use-cases/challenge-problem-2/cp2_scenarios/"

اضبط `--model=nondet` لإنشاء نسخة غير حتمية.

ينتج عن ذلك ملف maude القابل للتنفيذ (وملف HCS config json المقابل) في دليل الإخراج.
يجب أن يكون ملف التهيئة json المدخل سهل المتابعة. يتضمن تحديد:
 * طوبولوجيا الشبكة (الروابط وخصائصها)
 * الخصم (في هذه الحالة ملامح كاشف zeek، البيانات الأساسية لكاشفات المتوسط المتحرك، وتكويناتها)
 * القنوات/البروتوكولات: يتضمن كل بروتوكول شبكة غريبة وبروتوكول شبكة أساسي. الأول يخفي/يضمّن البيانات في الثاني. على سبيل المثال، Iodine يضمّن في DNS (لذا تسمى القناة iodine-dns) وDestini يضمّن في Mastodon

راجع [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/main/HCSParamsGuide.md) للحصول على وصف لبعض المعلمات.
لاحظ أن النموذج الاحتمالي سيجمع بين المعلمات غير الحتمية وكذلك المعلمات الاحتمالية (التي تتجاوز المعلمات غير الحتمية).

### استخدام تهيئة YML
#### تهيئات فردية
تحتوي تهيئة YML على التهيئة الكاملة للأنفاق والشبكات الأساسية. يمكننا إنشاء تهيئة HCS مباشرة منها.```shell
 maude-hcs --verbose  generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml     --model=prob --filename=generated_test_yml

التكوينات المجمعة لـ CP2

بالنسبة للتكوينات المجمعة مثل تلك الموجودة في CP2، قم بتحويل ملفات YML متعددة إلى ملفات سيناريو Maude:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]

حيث `scenario_dir` اختياري (القيمة الافتراضية هي `../pwnd_cp2`)

### استخدام تكوين Shadow yaml
يمكن تحديد تكوين الشبكة باستخدام ملف shadow بدلاً من ملف تكوين HCS json الخاص بنا
(انظر محاكي [Shadow](https://github.com/shadow/shadow) لمزيد من المعلومات حول مواصفات shadow).

لإنشاء نموذج يستخدم الخصائص المحددة في ملف shadow، حدد:```shell
--shadow-filename <path_to_shadow_file.yaml>

يحدد ملف yaml الخاص بـ shadow إعدادات الشبكة والمضيف والعمليات.

بافتراض أن إعداد شبكة shadow موجود في الدليل ../pwnd-cp1، قم بتشغيل```shell maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow

## تشغيل تكوينات HCS

### التشغيل المستقل باستخدام Maude
لتشغيل تكوين في maude المستقل، قم أولاً بتثبيت [standalone maude](https://github.com/maude-lang/Maude) لنظامك (نوصي بالإصدار 3.5.0 أو أقل)