raytheonbbn/maude-hcsФормальный фреймворк моделирования и анализа для скрытых систем связи, позволяющий специфицировать скрытые каналы, модели противника и выполнять статистическую проверку моделей компромисса между необнаружимостью и производительностью.
Maude-HCS — один из первых обобщенных и модульных инструментальных цепочек для формальной спецификации и рассуждения о скрытых системах связи (HCS) в реальных масштабах. Он позволяет разработчикам сетей быстро и эффективно исследовать альтернативные проекты HCS и предоставляет формальные гарантии конфиденциальности и производительности, необходимые для доверия к проекту.
Скрытые системы связи (HCS) встраивают скрытые сообщения в обычную сетевую активность, чтобы скрыть факт общения. На практике необнаруживаемость HCS обычно оценивается с помощью ad hoc статистики трафика или специальных детекторов, что делает утверждения о безопасности тесно связанными с экспериментальными установками и неявными предположениями о противнике.
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
Для виртуального окружения```bash
python -m venv venv
source venv/bin/activate
Мы структурировали исходный код репозитория так, чтобы импортировать dns-formalization-maude как зависимость (подмодуль). Мы создали форк этой зависимости, чтобы отслеживать наши изменения в ней. Мы используем sparse-checkout, чтобы избежать необходимости извлекать весь исходный код зависимости, который включает много ненужных файлов (например, Testbed).
Чтобы клонировать основной репозиторий```shell git clone [email protected]:raytheonbbn/maude-hcs.git
Ветка main содержит последний (возможно, нестабильный) исходный код.
Старые ветки/теги, такие как `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 .
## Авто-генерация пользовательских моделей
Пользовательские модели — это марковские модели, предназначенные для представления поведения пользователей.
Они представлены в формате 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/"
Мы генерируем начальные конфигурации с помощью команды 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/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, конвертируйте несколько YML-файлов в файлы сценариев Maude:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
Где `scenario_dir` является необязательным (по умолчанию `../pwnd_cp2`)