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} }
## आवश्यकताएँ
python संस्करण `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
virtual env के लिए```bash
python -m venv venv
source venv/bin/activate
We structured the repo source code so that we import dns-formalization-maude as a dependency (a submodule). We created a fork of this dependency so that we can track our changes to it. We use sparse-checkout to avoid needing to checkout all the source of the dependency which includes many irrelevant files (such as Testbed).
To clone the main repo```shell git clone [email protected]:raytheonbbn/maude-hcs.git
मुख्य शाखा में नवीनतम (संभवतः अस्थिर) स्रोत है।
`pwnd.cp1` जैसी पुरानी शाखाएँ/टैग स्थिर स्नैपशॉट को संदर्भित करते हैं जिनका उपयोग मूल्यांकन के दौरान परिणाम उत्पन्न करने के लिए किया गया था
(उदा., `pwnd.cp1` चैलेंज प्रॉब्लम 1 के लिए उपयोग किया गया, और इसी प्रकार `pwnd.cp2`)।
किसी पुराने स्नैपशॉट का उपयोग करने के लिए, विशिष्ट शाखा को चेकआउट करें (जैसे `pwnd.cp1`)।
हमारे कोड के क्लोन का उपयोग करके dns सबमॉड्यूल सेटअप करें ताकि हम मूल स्रोत में किए गए परिवर्तनों को ट्रैक कर सकें,
केवल प्रासंगिक स्रोत रखने के लिए स्पार्स-चेकआउट का उपयोग करें।```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 पर सेट करें।
उपरोक्त को .git/modules/maude_hcs/deps/dns_formalization/info/ के अंतर्गत sparse-checkout नामक एक नई फ़ाइल बनानी चाहिए
और इसे केवल Maude/src जैसी कुछ निर्देशिकाओं को शामिल करने का निर्देश देना चाहिए।
इस बिंदु पर git status एक साफ़ स्टार्ट दिखाना चाहिए।
इंस्टॉल करने के लिए, पहले dns नामक पैकेज के रूप में निर्भरता इंस्टॉल करें, हम इसे Maude.* के रूप में आयात करते हैं,
फिर maude_hcs को एक पैकेज के रूप में इंस्टॉल करें (dns पर निर्भरता के साथ)।```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## स्वचालित रूप से उपयोगकर्ता मॉडल उत्पन्न करें
उपयोगकर्ता मॉडल मार्कोव मॉडल होते हैं जिनका उद्देश्य यह दर्शाना है कि उपयोगकर्ता कैसे व्यवहार करते हैं।
ये json प्रारूप में दिए गए हैं।
पहला कदम इन्हें औपचारिक maude प्रस्तुतियों में परिवर्तित करना है।
ऐसा करने के लिए, निम्नलिखित निर्दिष्ट करें
- protocol: dns या mastodon
- input directory जिसमें वे सभी json मॉडल हैं जिन्हें आप कनवर्ट करना चाहते हैं
- output directory जिसमें json मॉडलों के सभी maude संस्करण होंगे
उदाहरण के लिए,```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/"
मार्कोव जेसन विनिर्देशों के उदाहरण ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/ के अंतर्गत देखें
(और इसी प्रकार मास्टोडॉन के लिए), साथ ही उनके रूपांतरित मौड विनिर्देशों के साथ।
हम generate कमांड का उपयोग करके प्रारंभिक कॉन्फ़िगरेशन उत्पन्न करते हैं।
HCS कॉन्फ़िगरेशन को सीधे HCS कॉन्फ़िगरेशन पैरामीटर का उपयोग करके जेसन में पास किया जा सकता है,
या Shadow प्रयोग कॉन्फ़िगरेशन फ़ाइल का उपयोग करके, या YML कॉन्फ़िगरेशन फ़ाइल का उपयोग करके।
इनमें से प्रत्येक का वर्णन आगे किया गया है।
maude-hcs json कॉन्फ़िगरेशन फ़ाइल को इस प्रकार पास करें,
आयोडीन के साथ एक प्रोबेबिलिस्टिक DNS मॉडल कॉन्फ़िगरेशन उत्पन्न करने और आउटपुट फ़ाइल नाम निर्दिष्ट करने के लिए,```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 डिटेक्टर प्रोफ़ाइल, मूविंग एवरेज डिटेक्टरों के लिए बेसलाइन डेटा, और उनके कॉन्फ़िगरेशन)
* चैनल/प्रोटोकॉल: प्रत्येक प्रोटोकॉल में एक weird नेटवर्क और एक अंतर्निहित नेटवर्क प्रोटोकॉल शामिल होता है। पहला दूसरे में डेटा छिपाता/एम्बेड करता है। उदाहरण के लिए, Iodine DNS में एम्बेड होता है (इसलिए चैनल को iodine-dns कहा जाता है) और Destini Mastodon में एम्बेड होता है
कुछ पैरामीटरों के विवरण के लिए [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/main/HCSParamsGuide.md) देखें।
ध्यान दें कि संभाव्य मॉडल गैर-निश्चयात्मक पैरामीटरों के साथ-साथ संभाव्य पैरामीटरों (जो गैर-निश्चयात्मक पैरामीटरों को ओवरराइड करते हैं) को भी जोड़ देगा।
### YML कॉन्फ़िगरेशन का उपयोग करना
#### एकल कॉन्फ़िगरेशन
एक YML कॉन्फ़िगरेशन में टनलों और अंतर्निहित नेटवर्कों का पूर्ण कॉन्फ़िगरेशन होता है।
हम इससे सीधे HCS config उत्पन्न कर सकते हैं।```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`)