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/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 вместо нашего JSON-файла конфигурации HCS
(См. симулятор [Shadow](https://github.com/shadow/shadow) для получения дополнительной информации о спецификациях shadow).
Чтобы создать модель, использующую характеристики, заданные в файле shadow, укажите:```shell
--shadow-filename <path_to_shadow_file.yaml>
Файл shadow yaml указывает конфигурации сети, хоста и процессов. Если конфигурация сети 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 сначала установите [автономный 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
The probabilistic model and its initial configuration should be specified in Maude and provided via the ``--test TEST`` option (default: ``results/generated_test.maude``).
The Maude execution starts from the initial term provided via the ``--initail INITIAL`` option (default: ``initConfig`` specified in ``TEST``) and rewrites to the final configuration.
From the final configuration, the observables are extracted using the monitor and adversary actors specified in the Maude source file for the model checking problem, provided via ``--file FILE`` option, or by the ``--protocol PR`` option.
For example ``--protocol dns`` refers to a model checking file created specifically for the dns protocol under `lib/`.
Quantitative properties, such as the expected value of the average latency, can be specified using a QuaTEx formula and provided via ``--query QUERY`` option (default: ``smc/query.quatex``).
Our example latency and scalability metrics in terms of exfiltrated files are defined in ``smc/latency.quatex`` and ``smc/scalability_cp2_scenario_1.quatex``, and imported into ``smc/cp2_eval_cp2_scenario_1.quatex``, and can be expressed with a QuaTEx formula of the following form:```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() извлекает значение задержки из монитора и оценивает его ожидание с delta=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