raytheonbbn/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
لقد قمنا بتنظيم شفرة مصدر المستودع بحيث نقوم باستيراد 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.
نقوم بإنشاء التكوينات الأولية باستخدام الأمر generate.
يمكن تمرير تكوينات HCS مباشرة بصيغة JSON باستخدام معلمات تكوين HCS،
أو باستخدام ملف تكوين تجربة Shadow، أو باستخدام ملف تكوين YML.
كل من هذه الطرق موصوفة فيما يلي.
مرر ملف تكوين 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/HEAD/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، قم بتحويل ملفات 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 أو أقل)
لتشغيل تكوين واحد، قم باستدعاء maude مع اسم الملف، على سبيل المثال، في `results`،```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
داخل موجه Maude، اكتب```shell rew initConfig .
سيؤدي هذا إلى تنفيذ جميع عمليات إعادة الكتابة حتى لا يتم العثور على المزيد من القواعد ولا يمكن تحقيق أي تقدم.
ستؤدي إضافة التسجيل إلى زيادة مستوى التفصيل في التنفيذ مع```shell
set print attribute on .
يمكن أيضًا التنقل خلال التنفيذ خطوة بخطوة باستخدام الأوامر التالية (راجع دليل Maude)```shell rew[1] initConfig . cont 1 .
### الفحص النموذجي الإحصائي
الفحص النموذجي الإحصائي متاح عبر الأمر الفرعي scheck في [QMaude](https://github.com/fadoss/umaudemc):```shell
maude-hcs scheck [-h] [--advise]
[--protocol {dns}] [--file FILE] [--test TEST] [--initial INITIAL] [--query QUERY]
[--assign METHOD] [--alpha ALPHA] [--delta DELTA]
[--seed SEED] [--jobs JOBS] [--format {text,json}]
options:
--help, -h Show help message and exit
--advise Do not suppress debug messages from Maude
--protocol PR The protocol module being analyzed e.g., dns, which points to an smc file specific to that protocol.
--file FILE Maude source file specifying the model-checking problem. If --protocol is specified, this parameter becomes optional, and if specified overrides the protocol smc file.
--test TEST Test generated from maude-hcs, default=results/generated_test.maude
--initial INITIAL Initial term, default=initConfig
--query QUERY QuaTEx query, default=smc/query.quatex
--assign METHOD Assign probabilities to the successors according to the given method, default=pmaude
--alpha ALPHA, -a ALPHA Required significance level for the confidence interval, default=0.05
--delta DELTA, -d DELTA Maximum admissible radius for the confidence interval around the mean, default=0.5
--seed SEED, -s SEED Random seed
--jobs JOBS, -j JOBS Number of parallel simulation threads, default=1, -j 0 will start as many jobs as CPU units
--format {text,json} Output format for the simulation results, default=text
--distribute WORKERS Distribute the computation across multiple machines, specified as a list of workers for the simulation.
--dump OUTPUTFILE Dump query evaluations into the given file. Currently, it only works with the sequential version (-j 1).
For each simulation, a line is written with the result of all queries separated by space.
-D D Define a constant to be used in QuaTEx expressions.
مثال على تشغيل SMC للملف الذي تم إنشاؤه بواسطة الأمر أعلاه هو:```shell maude-hcs scheck --test ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude --query ./smc/cp2_eval_cp2_scenario_1.quatex -j 0 -n 30-120
النموذج الاحتمالي وتكوينه الأولي يجب تحديدهما في Maude وتوفيرهما عبر الخيار ``--test TEST`` (الافتراضي: ``results/generated_test.maude``).
تنفيذ Maude يبدأ من المصطلح الأولي المقدم عبر الخيار ``--initail INITIAL`` (الافتراضي: ``initConfig`` المحدد في ``TEST``) ويعيد الكتابة إلى التهيئة النهائية.
من التهيئة النهائية، يتم استخراج القيم القابلة للملاحظة باستخدام مراقب وأطراف الخصم المحددة في ملف مصدر Maude لمشكلة التحقق من النموذج، المقدم عبر الخيار ``--file FILE``، أو عبر الخيار ``--protocol PR``.
على سبيل المثال ``--protocol dns`` يشير إلى ملف التحقق من النموذج الذي تم إنشاؤه خصيصًا لبروتوكول dns تحت `lib/`.
يمكن تحديد الخصائص الكمية، مثل القيمة المتوقعة لمتوسط زمن الاستجابة، باستخدام صيغة QuaTEx وتوفيرها عبر الخيار ``--query QUERY`` (الافتراضي: ``smc/query.quatex``).
مقاييس زمن الاستجابة وقابلية التوسع في مثالنا من حيث الملفات المسربة محددة في ``smc/latency.quatex`` و ``smc/scalability_cp2_scenario_1.quatex``، ومستوردة إلى ``smc/cp2_eval_cp2_scenario_1.quatex``، ويمكن التعبير عنها بصيغة QuaTEx بالشكل التالي:```shell
Latency() = s.rval("getLatency(getMonitor(C))");
eval E[Latency()] with delta = 2;
ExfilFilesC2() =
if (s.rval("getToDCumulativeNQueryPostNAT(C,416)") == 0.0) then
discard
else
s.rval("getExfilFiles(getMonitor(C), getToDCumulativeNQueryPostNAT(C,416))")
fi;
eval E[ExfilFilesC2()];
حيث يستخرج التعبير Latency() قيمة الكمون من المراقب ويُقيِّم توقعه مع دلتا = 2.
يقوم التعبير ExfilFilesC2() بتقييم عدد الملفات المسربة بشكل شرطي:
إذا كان وقت الكشف بناءً على العدد التراكمي لاستعلامات DNS بعد NAT هو صفر - مما يعني عدم حدوث كشف لأن العدد التراكمي للاستعلامات لا يتجاوز عتبته (مثل 416 في المثال أعلاه) - يتم تجاهل العينة؛
وإلا، يتم تقييم عدد الملفات المسربة حتى وقت الكشف.
يستمر أخذ العينات حتى يتم الوصول إلى العدد المحدد من العينات (أي خيار -n min-max، مثل -n 30-300) أو يتم الإجابة على جميع الاستعلامات بمستوى الدلالة الإحصائية المطلوب.
في المثال أدناه، يتم الإجابة على الاستعلام الثاني بعد 30 عينة باستخدام القيم الافتراضية alpha=0.05 و delta=0.5، بينما يتم الإجابة على الاستعلام الأول بعد 270 عينة باستخدام with delta = 2، كما هو محدد أعلاه.
يتضمن الناتج:
إذا قمنا بتعديل قيمة العتبة في صيغة QuaTEx أعلاه إلى 500، فسيتم تجاهل بعض العينات.
ثم يتم الإبلاغ عن النتائج مع عدد العينات المهملة، ويتم حساب الضمانات الإحصائية باستخدام العينات المتبقية كما هو موضح أدناه.```shell
Number of simulations = 270
Query 1 (./smc/readme.quatex:7:1)
μ = 191.80187664851906 σ = 16.429217228790975 r = 1.9685272804723886
Query 2 (./smc/readme.quatex:8:1) (39 simulations)
μ = 9.76923076923077 σ = 0.48458003855418535 r = 0.1570826767676969
where 21 executions out of 60 (35.0%) have been discarded
لإعادة إنتاج نفس التجارب ضمن نفس إعداد التوازي (أي نفس قيمة -j)، استخدم خيار --seed بنفس البذرة العشوائية. بشكل افتراضي أو عند تمرير ‑1، يتم استخدام الوقت الحالي كبذرة.```shell
Number of simulations = 30 μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
Number of simulations = 30 μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
Number of simulations = 30 μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
Number of simulations = 30 μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
### أتمتة الاختبار
runexp.sh هو سكريبت أتمتة يجمع بين التوليد وتحليل SMC. يتطلب وسيطتين إلزاميتين:```shell
runexp.sh CONFIG_FILENAME METRIC
where
CONFIG_FILENAME is the name of the .yaml shadow file defining the experiment
METRIC is the quatex property and can be latency, throughput, goodput, or all
يمكن توازي SMC بشكل كبير باستخدام جميع النوى على الجهاز للحصول على تسريع خطي تقريبًا في أخذ العينات بطريقة مونت كارلو، باستخدام الخيار -j 0 كما هو موضح أعلاه.
يتيح QMaude توازيًا أكبر عبر الأجهزة باستخدام SMC الموزع (الميزة لا تزال قيد الاختبار النشط)
لتشغيل SMC الموزع، يجب أن يكون هناك عامل واحد أو أكثر يتم تشغيلهم باستخدام
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
الخيارات الوحيدة لأمر sworker الجديد هي العنوان (-a) والمنفذ (-p). يبقى في انتظار الاتصالات من وحدة التحكم.
على جانب وحدة التحكم، يمكن تنفيذ أمر scheck عادي مع خيار إضافي --distribute . على سبيل المثال،
$ maude-hcs scheck --distribute workers.json
يحدد ملف workers.json (يمكن أيضًا أن يكون TOML أو YAML) قائمة العمال للمحاكاة. يجب أن يكون هذا الملف قاموسًا بمفتاح workers يحتوي على قائمة من القيم بالشكل { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } أو ببساطة { "workers": [ "127.0.0.1:1234" ] }. بخلاف ذلك، يجب أن تكون الخيارات والمخرجات مماثلة لأمر scheck العادي.
سيتصل أمر scheck بالعمال البعيدين، ويمرر لهم جميع المعلومات التي يحتاجونها، وينشطهم، ويعالج نتائجهم حتى يتم الوصول إلى مستوى الثقة المطلوب. بدلاً من نسخ الملفات يدويًا إلى كل جهاز يشغل عاملًا، يتم إرسال الملفات عبر الاتصال. يتم حل تضمينات Maude وإرسال نسخة مسطحة من مصادر Maude.
يقدم QMaude التحقق الإحصائي للنماذج (SMC) للنموذج بنفس الشكلية.
انسخ latency.quatex و smc.maude إلى دليل تجربتك (أو احتفظ به في results).
قم بتعديل الأول لتحميل التجربة المستهدفة (الاحتمالية).
تشغيل```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
تقوم QMaude بإرجاع القيمة المتوقعة لاستعلامات quatex (μ) وعدد محاكاة مونت كارلو التي استغرقتها للوصول إلى تلك القيمة.
## اختبارات
لتشغيل الاختبارات، قم أولاً بتثبيت pytest في بيئتك.```
pip install -e .[test]
ثم قم بتشغيل اختبارات الوحدة``` python -m pytest
## أدوات مساعدة أخرى
لتحويل دليل من الصور إلى ملف بيانات وصفية بتنسيق JSON يُستخدم في التجربة،
على سبيل المثال، لإنشاء الصور التي يستخدمها عميل mastodon tgen (وبالمثل صور الغلاف لـ destini)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
استخدم plotfinal.py مع الوسائط smc_directory, tne_directory, quatex_directory```shell
python scripts/plotfinal.py use-cases/challenge-problem-2/results-aligned/ use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/ smc/
سوف يقوم نفس البرنامج النصي بإنشاء مخططات CDF.```shell
python scripts/gather\_samples.py use-cases/challenge-problem-2/results-aligned/samples/ use-cases/challenge-problem-2/results-aligned/cdfs use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/
المشاريع التالية تُستخدم مباشرة بواسطة Maude-HCS