Maude-HCS

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.

Introduction

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

Installer : depuis la source git

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.

Générer automatiquement les configurations HCS

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.

Utilisation de la configuration json HCS

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/main/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).