raytheonbbn/maude-hcsCadre de modélisation et d'analyse formelle pour les systèmes de communication cachés, permettant la spécification de canaux cachés, de modèles adverses, et la vérification statistique des compromis entre indétectabilité et performance.
Maude-HCS est l'une des premières chaînes d'outils généralisées et modulaires pour spécifier formellement et raisonner sur les systèmes de communication cachés (HCS) à l'échelle réelle. Elle permet aux concepteurs de réseaux d'explorer rapidement et efficacement différentes conceptions de HCS et fournit les garanties formelles de confidentialité-performance nécessaires pour faire confiance à la conception.
Les systèmes de communication cachés (HCS) intègrent des messages secrets dans l'activité réseau ordinaire pour dissimuler la présence de communication. En pratique, l'indétectabilité d'un HCS est généralement évaluée à l'aide de statistiques de trafic ad hoc ou de détecteurs spécifiques, rendant les affirmations de sécurité étroitement liées aux configurations expérimentales et aux hypothèses adverses implicites.
Maude-HCS est un cadre de modélisation et d'analyse exécutable qui fournit une base princière et exécutable pour raisonner sur les compromis indétectabilité–performance dans les conceptions complexes de HCS. Les concepteurs spécifient formellement le comportement du protocole, les observables de l'adversaire et les hypothèses environnementales, et génèrent des échantillons de Monte Carlo à partir des distributions de traces induites. Ceux-ci peuvent être utilisés pour auditer les affirmations d'indétectabilité en estimant les taux de vrais et faux positifs de un test statistique et en convertissant ces estimations en bornes inférieures sur les mesures d'indétectabilité. Cela permet une évaluation systématique de la détectabilité et de ses compromis avec la performance sous des hypothèses de modélisation explicitement énoncées.
N'hésitez pas à nous contacter si vous avez besoin d'aide pour modéliser et raisonner sur votre HCS. Et veuillez envisager de citer nos travaux si vous les utilisez dans le cadre de votre recherche.```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} }
## Prérequis
Nécessite python version `3.12.4`
Créez votre environnement préféré et activez-le, par exemple
Pour pyenv```bash
pyenv install 3.12.4
pyenv local 3.12.4
Pour conda```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2
Pour l'environnement virtuel```bash
python -m venv venv
source venv/bin/activate
Nous avons structuré le code source du dépôt de manière à importer dns-formalization-maude comme dépendance (un submodule). Nous avons créé un fork de cette dépendance afin de suivre nos modifications à celle-ci. Nous utilisons sparse-checkout pour éviter de devoir vérifier l'intégralité de la source de la dépendance qui contient de nombreux fichiers non pertinents (comme Testbed).
Pour cloner le dépôt principal```shell git clone [email protected]:raytheonbbn/maude-hcs.git
La branche principale contient la source la plus récente (possiblement instable).
Les branches ou tags plus anciens, comme `pwnd.cp1`, font référence à des instantanés stables utilisés pour produire des résultats lors des évaluations
(par exemple, `pwnd.cp1` utilisé pour le problème de défi 1, et de même `pwnd.cp2`).
Pour utiliser un instantané plus ancien, extrayez la branche spécifique (par exemple `pwnd.cp1`).
Configurez le sous-module dns en utilisant notre clone du code afin de pouvoir suivre les modifications apportées à la source d'origine, utilisez sparse-checkout pour ne conserver que les sources pertinentes```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
Dans la commande ci-dessus, définissez <branch> soit sur pwnd.43.rb1 pour reproduire les résultats du problème 1 du défi,
soit sur pwnd pour la dernière version.
Ce qui précède doit créer un nouveau fichier nommé sparse-checkout sous
.git/modules/maude_hcs/deps/dns_formalization/info/
et lui indiquer de n'inclure que certains répertoires tels que Maude/src.
À ce stade, git status doit afficher un état propre.
Pour installer, installez d'abord la dépendance en tant que package appelé dns, que nous importons sous Maude.*,
puis installez maude_hcs en tant que package (avec dépendance sur dns).```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## Générer automatiquement des modèles d'utilisateurs
Les modèles d'utilisateurs sont des modèles de Markov destinés à représenter le comportement des utilisateurs.
Ils sont fournis au format JSON.
La première étape consiste à les convertir en représentations formelles Maude.
Pour ce faire, spécifiez les
- protocole : dns ou mastodon
- répertoire d'entrée contenant tous les modèles json que vous souhaitez convertir
- répertoire de sortie qui contiendra toutes les versions maude des modèles json
Par exemple,```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/"
Voir les exemples de spécifications markov json sous ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
(et de même pour mastodon), ainsi que leurs spécifications maude converties.
Nous générons les configurations initiales à l'aide de la commande generate.
Les configurations HCS peuvent être directement passées en json en utilisant les paramètres de configuration HCS, ou en utilisant un fichier de configuration d'expérience Shadow, ou en utilisant un fichier de configuration YML. Chacune de ces méthodes est décrite ci-après.
Passez un fichier de configuration json maude-hcs comme suit,
Pour générer une configuration de modèle DNS probabiliste avec iodine et spécifier le nom du fichier de sortie,```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/"
Set `--model=nondet` to generate a nondeterministic version.
This produces the executable maude file (and the corresponding HCS config json) in the output directory.
The input json configuration file should be straightforward to follow. It includes specification of
* network topology (links and their characteristics)
* adversary (in this case zeek detector profiles, baseline data for moving average detectors, and their configurations)
* channels/protocols: each protocol includes a weird network and an underlying network protocol. The former hides/embeds data into the latter. For example, Iodine embeds in DNS (so the channel is called iodine-dns) and Destini embeds in Mastodon
Refer to [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/HEAD/HCSParamsGuide.md) for a description of some of the parameters.
Note that probabilistic model will combine the nondeterministic params as well as the
probabilistic params (which override the nondeterministic ones).
### Using a YML configuration
#### Single configurations
A YML configuration contains the full config of the tunnels and undelying networks.
We can generate an HCS config directly from it.```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
Pour les configurations par lots comme celles de CP2, convertissez plusieurs fichiers YML en fichiers de scénario Maude :```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
Où `scenario_dir` est optionnel (par défaut `../pwnd_cp2`)
### Utilisation de la configuration yaml Shadow
La configuration réseau peut être spécifiée à l'aide d'un fichier shadow au lieu de notre fichier json de configuration HCS
(Voir le simulateur [Shadow](https://github.com/shadow/shadow) pour plus d'informations sur les spécifications shadow).
Pour générer un modèle qui utilise les caractéristiques définies dans un fichier shadow, spécifiez :```shell
--shadow-filename <path_to_shadow_file.yaml>
Le fichier yaml shadow spécifie les configurations réseau, hôte et processus.
En supposant que la configuration réseau shadow se trouve dans le répertoire ../pwnd-cp1, exécutez```shell
maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow
## Exécuter les configurations HCS
### Exécution autonome avec Maude
Pour exécuter une configuration en maude autonome, installez d'abord [standalone maude](https://github.com/maude-lang/Maude) pour votre système (nous recommandons la version 3.5.0 ou inférieure)
Pour exécuter une seule configuration, invoquez maude avec le nom du fichier, par exemple, dans `results`,```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
Dans l'invite Maude, tapez```shell rew initConfig .
Cela exécutera toutes les réécritures jusqu'à ce qu'aucune autre règle ne soit trouvée et qu'aucun progrès ne puisse être réalisé.
L'ajout de la journalisation augmentera la verbosité de l'exécution avec```shell
set print attribute on .
L'exécution peut également être parcourue pas à pas avec les commandes suivantes (reportez-vous au manuel maude)```shell rew[1] initConfig . cont 1 .
### Vérification Statistique de Modèles
La vérification statistique de modèles est disponible via la sous-commande scheck dans [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.
Un exemple d'exécution SMC pour le fichier généré par la commande ci-dessus est :```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
Le modèle probabiliste et sa configuration initiale doivent être spécifiés en Maude et fournis via l'option ``--test TEST`` (par défaut : ``results/generated_test.maude``).
L'exécution Maude commence à partir du terme initial fourni via l'option ``--initail INITIAL`` (par défaut : ``initConfig`` spécifié dans ``TEST``) et réécrit vers la configuration finale.
À partir de la configuration finale, les observables sont extraits à l'aide des acteurs de surveillance et d'adversaire spécifiés dans le fichier source Maude pour le problème de model checking, fourni via l'option ``--file FILE``, ou par l'option ``--protocol PR``.
Par exemple, ``--protocol dns`` fait référence à un fichier de model checking créé spécifiquement pour le protocole DNS sous `lib/`.
Les propriétés quantitatives, telles que la valeur attendue de la latence moyenne, peuvent être spécifiées à l'aide d'une formule QuaTEx et fournies via l'option ``--query QUERY`` (par défaut : ``smc/query.quatex``).
Nos exemples de métriques de latence et de passage à l'échelle en termes de fichiers exfiltrés sont définis dans ``smc/latency.quatex`` et ``smc/scalability_cp2_scenario_1.quatex``, et importés dans ``smc/cp2_eval_cp2_scenario_1.quatex``, et peuvent être exprimés avec une formule QuaTEx de la forme suivante :```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()];
où l'expression Latency() extrait la valeur de latence du moniteur et évalue son espérance avec delta = 2.
L'expression ExfilFilesC2() évalue conditionnellement le nombre de fichiers exfiltrés :
Si le temps de détection basé sur le nombre cumulatif de requêtes DNS post-NAT est nul - ce qui signifie qu'aucune détection ne se produit car le nombre cumulatif de requêtes ne dépasse jamais son seuil (par exemple, 416 dans l'exemple ci-dessus) - l'échantillon est rejeté ;
sinon, le nombre de fichiers exfiltrés jusqu'au moment de la détection est évalué.
L'échantillonnage continue jusqu'à ce que le nombre d'échantillons spécifié soit atteint (c'est-à-dire l'option -n min-max, comme -n 30-300) ou que toutes les requêtes soient répondues avec la significativité statistique souhaitée.
Dans l'exemple ci-dessous, la deuxième requête est répondue après 30 échantillons en utilisant les valeurs par défaut alpha=0.05 et delta=0.5, tandis que la première requête est répondue après 270 échantillons en utilisant with delta = 2, comme spécifié ci-dessus.
La sortie inclut :
Si nous modifions la valeur de seuil dans la formule QuaTEx ci-dessus à 500, certains échantillons sont écartés.
Les résultats sont alors rapportés avec le nombre d'échantillons écartés, et les garanties statistiques sont calculées à l'aide des échantillons restants comme indiqué ci-dessous.```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
Pour reproduire les mêmes expériences dans le même réglage de parallélisation (c'est-à-dire la même valeur de -j), utilisez l'option --seed avec la même graine aléatoire.
Par défaut ou lors du passage de ‑1, l'heure actuelle est utilisée comme graine.```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
### Automatisation des tests
runexp.sh est un script d'automatisation qui combine la génération et l'analyse SMC. Il prend deux arguments obligatoires :```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
Le SMC est hautement parallélisable en utilisant tous les cœurs de la machine pour obtenir une accélération quasi linéaire dans l'échantillonnage de Monte Carlo, en utilisant l'option -j 0 comme indiqué ci-dessus.
QMaude permet encore plus de parallélisme entre machines en utilisant le SMC distribué (fonctionnalité encore en test actif).
Pour exécuter le SMC distribué, un ou plusieurs workers doivent être démarrés avec
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
Les seules options pour la nouvelle commande sworker sont l'adresse (-a) et le port (-p). Elle reste en attente de connexions de la part du contrôleur.
Du côté du contrôleur, une commande scheck ordinaire peut être exécutée avec une option supplémentaire --distribute . Par exemple,
$ maude-hcs scheck --distribute workers.json
Le fichier workers.json (il peut également être en TOML ou YAML) spécifie la liste des workers pour la simulation. Ce fichier doit être un dictionnaire avec une clé workers contenant une liste de valeurs de la forme { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } ou simplement { "workers": [ "127.0.0.1:1234" ] }. Hormis cela, les options et la sortie devraient être les mêmes que pour la commande scheck classique.
La commande scheck se connectera aux workers distants, leur transmettra toutes les informations nécessaires, les activera et traitera leurs résultats jusqu'à ce que le niveau de confiance prescrit soit atteint. Au lieu de copier manuellement les fichiers sur chaque machine exécutant un worker, les fichiers sont envoyés par la connexion. Les inclusions Maude sont résolues et une version aplatie des sources Maude est envoyée.
QMaude offre la vérification statistique de modèles (SMC) du modèle dans le même formalisme.
Copiez latency.quatex et smc.maude dans le répertoire de votre expérience (ou gardez-les dans results).
Modifiez le premier pour charger l'expérience cible (probabiliste).
Exécutez```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaude renvoie la valeur attendue pour les requêtes quatex (μ), et le nombre de simulations Monte Carlo nécessaires pour atteindre cette valeur.
## Tests
Pour exécuter les tests, installez d'abord pytest dans votre environnement.```
pip install -e .[test]
Ensuite, exécutez les tests unitaires.``` python -m pytest
## Autres utilitaires
Pour convertir un répertoire d'images en un fichier de métadonnées json utilisé dans l'expérience,
Par exemple pour générer les images utilisées par le client mastodon tgen (de même pour les images de couverture pour destini)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
Utilisez plotfinal.py avec les arguments 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/
Le même script générera les graphiques 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/
Les projets suivants sont directement utilisés par Maude-HCS