raytheonbbn/maude-hcsFormales Modellierungs- und Analyseframework für versteckte Kommunikationssysteme, das die Spezifikation von verdeckten Kanälen, Angreifermodellen und statistischer Modellprüfung von Undetectability-Performance-Abwägungen ermöglicht.
Maude-HCS ist eine der ersten generalisierten und modularen Toolchains zur formalen Spezifikation und Analyse von Hidden Communication Systems (HCS) in realen Größenordnungen. Es ermöglicht Netzwerkdesignern, alternative HCS-Entwürfe schnell und effektiv zu erkunden und liefert formale Garantien für Privatsphäre und Leistung, die für das Vertrauen in den Entwurf erforderlich sind.
Hidden Communication Systems (HCS) betten verdeckte Nachrichten in gewöhnliche Netzwerkaktivitäten ein, um das Vorhandensein von Kommunikation zu verbergen. In der Praxis wird die Undurchschaubarkeit eines HCS typischerweise mit ad-hoc-Verkehrsstatistiken oder spezifischen Detektoren bewertet, was Sicherheitsaussagen eng an experimentelle Aufbauten und implizite gegnerische Annahmen koppelt.
Maude-HCS ist ein ausführbares Modellierungs- und Analyseframework, das eine prinzipielle und ausführbare Grundlage für die Analyse von Undurchschaubarkeits-Leistungs-Kompromissen in komplexen HCS-Entwürfen bietet. Designer spezifizieren formal das Protokollverhalten, gegnerische Beobachtungsgrößen und Umgebungsannahmen und generieren Monte-Carlo-Stichproben aus den induzierten Spurenverteilungen. Diese können verwendet werden, um Behauptungen über Undurchschaubarkeit zu überprüfen, indem die Raten der wahren und falschen Positiven eines statistischen Tests geschätzt und diese Schätzungen in untere Schranken für Undurchschaubarkeitsmaße umgewandelt werden. Dies ermöglicht die systematische Bewertung der Erkennbarkeit und ihrer Kompromisse mit der Leistung unter explizit genannten Modellierungsannahmen.
Bitte kontaktieren Sie uns, wenn Sie Hilfe bei der Modellierung und Analyse Ihres HCS benötigen. Und bitte erwägen Sie, unsere Arbeit zu zitieren, wenn Sie sie im Rahmen Ihrer Forschung verwenden.```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} }
## Anforderungen
Erfordert Python-Version `3.12.4`
Erstellen Sie Ihre bevorzugte Umgebung und aktivieren Sie sie, zum Beispiel
Für pyenv```bash
pyenv install 3.12.4
pyenv local 3.12.4
Für conda```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2
Für virtuelle Umgebung```bash
python -m venv venv
source venv/bin/activate
Wir haben den Quellcode des Repos so strukturiert, dass wir dns-formalization-maude als Abhängigkeit (ein Submodul) importieren. Wir haben einen Fork dieser Abhängigkeit erstellt, damit wir unsere Änderungen daran verfolgen können. Wir verwenden sparse-checkout, um nicht den gesamten Quellcode der Abhängigkeit auschecken zu müssen, der viele irrelevante Dateien (wie Testbed) enthält.
Um das Haupt-Repo zu klonen```shell git clone [email protected]:raytheonbbn/maude-hcs.git
Der Hauptzweig enthält die neueste (möglicherweise instabile) Quelle.
Ältere Branches/Tags wie `pwnd.cp1` beziehen sich auf stabile Snapshots, die zur Erzeugung von Ergebnissen während Evaluationen verwendet wurden
(z.B. `pwnd.cp1` für Challenge-Problem 1, und ähnlich `pwnd.cp2`).
Um einen älteren Snapshot zu verwenden, checkout den entsprechenden Branch (z.B. `pwnd.cp1`).
Richte das dns-Submodul mit unserem Klon des Codes ein, damit wir Änderungen an der Originalquelle nachverfolgen können, verwende sparse-checkout, um nur relevante Quellen zu behalten```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
In dem obigen Befehl setzen Sie <branch> entweder auf pwnd.43.rb1, um die Ergebnisse von Challenge-Problem 1 zu reproduzieren,
oder auf pwnd für die neueste Version.
Der obige Schritt sollte eine neue Datei namens sparse-checkout unter
.git/modules/maude_hcs/deps/dns_formalization/info/
erstellen und anweisen, nur bestimmte Verzeichnisse wie Maude/src einzuschließen.
An diesem Punkt sollte git status einen sauberen Start anzeigen.
Zur Installation installieren Sie zuerst die Abhängigkeit als ein Paket namens dns, wir importieren als Maude.*
dann installieren Sie maude_hcs als ein Paket (mit Abhängigkeit von dns).```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## Automatisch Benutzermodelle generieren
Benutzermodelle sind Markov-Modelle, die dazu dienen, das Verhalten von Benutzern abzubilden.
Diese werden im JSON-Format bereitgestellt.
Der erste Schritt besteht darin, diese in formale Maude-Repräsentationen zu konvertieren.
Dazu geben Sie Folgendes an:
- das Protokoll: dns oder mastodon
- das Eingabeverzeichnis, das alle JSON-Modelle enthält, die Sie konvertieren möchten
- das Ausgabeverzeichnis, das alle Maude-Versionen der JSON-Modelle enthalten wird
Zum Beispiel,```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/"
Siehe Beispiel-Markov-JSON-Spezifikationen unter ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
(und ähnlich für Mastodon), zusammen mit ihren konvertierten Maude-Spezifikationen.
Wir generieren Anfangskonfigurationen mit dem Befehl generate.
HCS-Konfigurationen können direkt im JSON-Format übergeben werden, indem HCS-Konfigurationsparameter verwendet werden,
oder eine Shadow-Experiment-Konfigurationsdatei oder eine YML-Konfigurationsdatei verwendet wird.
Jede dieser Methoden wird im Folgenden beschrieben.
Übergeben Sie eine maude-hcs-JSON-Konfigurationsdatei wie folgt:
Um eine probabilistische DNS-Modellkonfiguration mit iodine zu generieren und den Ausgabedateinamen anzugeben,```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`, um eine nichtdeterministische Version zu generieren.
Dies erzeugt die ausführbare Maude-Datei (und die entsprechende HCS-Konfigurations-JSON) im Ausgabeverzeichnis.
Die Eingabe-JSON-Konfigurationsdatei sollte einfach zu verstehen sein. Sie enthält Spezifikationen von
* Netzwerktopologie (Verbindungen und deren Eigenschaften)
* Gegner (in diesem Fall Zeek-Detektorprofile, Baseline-Daten für gleitende Durchschnittsdetektoren und deren Konfigurationen)
* Kanäle/Protokolle: Jedes Protokoll beinhaltet ein weirdes Netzwerk und ein zugrunde liegendes Netzwerkprotokoll. Ersteres versteckt/bettet Daten in Letzteres ein. Zum Beispiel bettet Iodine in DNS ein (daher heißt der Kanal iodine-dns) und Destini in Mastodon
Informationen zu einigen Parametern finden Sie im [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/HEAD/HCSParamsGuide.md).
Beachten Sie, dass das probabilistische Modell die nichtdeterministischen sowie die probabilistischen Parameter kombiniert (welche die nichtdeterministischen überschreiben).
### Using a YML configuration
#### Single configurations
Eine YML-Konfiguration enthält die vollständige Konfiguration der Tunnel und der zugrunde liegenden Netzwerke.
Wir können daraus direkt eine HCS-Konfiguration generieren.```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
Für Batch-Konfigurationen wie die in CP2, konvertieren Sie mehrere YML-Dateien in Maude-Szenariodateien:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
Wo `scenario_dir` optional ist (Standardwert `../pwnd_cp2`)
### Verwendung der Shadow-YAML-Konfiguration
Die Netzwerkkonfiguration kann mithilfe einer Shadow-Datei anstelle unserer HCS-Konfigurations-JSON angegeben werden
(Siehe [Shadow](https://github.com/shadow/shadow)-Simulator für weitere Informationen zu Shadow-Spezifikationen).
Um ein Modell zu generieren, das in einer Shadow-Datei definierte Merkmale verwendet, geben Sie Folgendes an:```shell
--shadow-filename <path_to_shadow_file.yaml>
Die Shadow-YAML-Datei spezifiziert die Netzwerk-, Host- und Prozesskonfigurationen.
Angenommen, die Shadow-Netzwerkkonfiguration befindet sich im Verzeichnis ../pwnd-cp1, führe```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-Konfigurationen ausführen
### Standalone-Ausführung mit Maude
Um eine Konfiguration mit standalone Maude auszuführen, installieren Sie zuerst [standalone maude](https://github.com/maude-lang/Maude) für Ihr System (wir empfehlen Version 3.5.0 oder niedriger)
Um eine einzelne Konfiguration auszuführen, rufen Sie maude mit dem Dateinamen auf, z. B. in `results`,```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
Geben Sie im Maude-Prompt ein:```shell rew initConfig .
Dies wird alle Umschreibungen ausführen, bis keine Regeln mehr gefunden werden und kein Fortschritt mehr erzielt werden kann.
Die Hinzufügung von Protokollierung wird die Ausführlichkeit der Ausführung mit```shell
set print attribute on .
Die Ausführung kann auch mit den folgenden Befehlen schrittweise durchgeführt werden (siehe das maude-Handbuch)```shell rew[1] initConfig . cont 1 .
### Statistische Modellprüfung
Die statistische Modellprüfung ist mittels des Unterbefehls scheck in [QMaude](https://github.com/fadoss/umaudemc) verfügbar:```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.
Ein beispielhafter SMC-Lauf für die von obigem Befehl generierte Datei ist:```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
Das probabilistische Modell und seine anfängliche Konfiguration sollten in Maude spezifiziert und über die Option ``--test TEST`` (Standard: ``results/generated_test.maude``) bereitgestellt werden.
Die Maude-Ausführung beginnt mit dem über die Option ``--initail INITIAL`` bereitgestellten Anfangsterm (Standard: ``initConfig``, angegeben in ``TEST``) und schreibt zur endgültigen Konfiguration um.
Aus der endgültigen Konfiguration werden die Observablen unter Verwendung des Monitors und der Gegenspieler-Akteure extrahiert, die in der Maude-Quelldatei für das Model-Checking-Problem angegeben sind, bereitgestellt über die Option ``--file FILE`` oder über die Option ``--protocol PR``.
Beispielsweise bezieht sich ``--protocol dns`` auf eine speziell für das dns-Protokoll erstellte Model-Checking-Datei unter `lib/`.
Quantitative Eigenschaften, wie der erwartete Wert der durchschnittlichen Latenz, können mit einer QuaTEx-Formel spezifiziert und über die Option ``--query QUERY`` (Standard: ``smc/query.quatex``) bereitgestellt werden.
Unsere Beispielmetriken für Latenz und Skalierbarkeit in Bezug auf exfiltrierte Dateien sind in ``smc/latency.quatex`` und ``smc/scalability_cp2_scenario_1.quatex`` definiert und in ``smc/cp2_eval_cp2_scenario_1.quatex`` importiert und können mit einer QuaTEx-Formel der folgenden Form ausgedrückt werden:```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()];
wo der Ausdruck Latency() den Latenzwert aus dem Monitor extrahiert und dessen Erwartung mit delta = 2 bewertet.
Der Ausdruck ExfilFilesC2() bewertet bedingt die Anzahl der exfiltrierten Dateien:
Wenn die Erkennungszeit basierend auf der kumulativen Anzahl von DNS-Abfragen nach NAT null ist – das heißt, dass keine Erkennung erfolgt, weil die kumulative Abfrageanzahl nie ihren Schwellenwert überschreitet (z. B. 416 im obigen Beispiel) – wird die Stichprobe verworfen;
andernfalls wird die Anzahl der bis zum Erkennungszeitpunkt exfiltrierten Dateien bewertet.
Die Stichprobennahme wird fortgesetzt, bis entweder die angegebene Anzahl von Stichproben erreicht ist (d. h. die Option -n min-max, wie z. B. -n 30-300) oder alle Abfragen mit der gewünschten statistischen Signifikanz beantwortet sind.
Im folgenden Beispiel wird die zweite Abfrage nach 30 Stichproben mit den Standardwerten alpha=0.05 und delta=0.5 beantwortet, während die erste Abfrage nach 270 Stichproben mit with delta = 2, wie oben angegeben, beantwortet wird.
Die Ausgabe umfasst:
Wenn wir den Schwellenwert in der obigen QuaTEx-Formel auf 500 ändern, werden einige Stichproben verworfen.
Die Ergebnisse werden dann zusammen mit der Anzahl der verworfenen Stichproben gemeldet, und die statistischen Garantien werden mit den verbleibenden Stichproben berechnet, wie unten gezeigt.```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
Um die gleichen Experimente innerhalb der gleichen Parallelisierungseinstellung (d.h. dem gleichen Wert von -j) zu reproduzieren, verwenden Sie die Option --seed mit dem gleichen Zufallsseed. Standardmäßig oder bei Angabe von ‑1 wird die aktuelle Zeit als Seed verwendet.```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
### Testautomatisierung
runexp.sh ist ein Automatisierungsskript, das Generierung und SMC-Analyse kombiniert. Es benötigt zwei erforderliche Argumente:```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 ist hochgradig parallelisierbar, indem alle Kerne der Maschine genutzt werden, um eine nahezu lineare Beschleunigung bei der Monte-Carlo-Stichprobenziehung zu erreichen, wie oben mit der Option -j 0 angegeben.
QMaude ermöglicht noch mehr Parallelität zwischen Maschinen mittels verteiltem SMC (Funktion noch im aktiven Test).
Um das verteilte SMC auszuführen, sollten ein oder mehrere Worker mit folgendem Befehl gestartet werden:
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Hört auf 127.0.0.1:1234...
Die einzigen Optionen für den neuen Befehl sworker sind die Adresse (-a) und der Port (-p). Er wartet dauerhaft auf Verbindungen vom Controller.
Auf der Controllerseite kann ein gewöhnlicher scheck-Befehl mit der zusätzlichen Option --distribute <Datei> ausgeführt werden. Zum Beispiel:
$ maude-hcs scheck --distribute workers.json
Die Datei workers.json (es kann auch TOML oder YAML sein) gibt die Liste der Worker für die Simulation an. Diese Datei sollte ein Wörterbuch mit einem Schlüssel workers sein, der eine Liste von Werten der Form { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } oder einfach { "workers": [ "127.0.0.1:1234" ] } enthält. Ansonsten sollten die Optionen und die Ausgabe dieselben wie beim regulären scheck-Befehl sein.
Der scheck-Befehl verbindet sich mit den entfernten Workern, übergibt ihnen alle benötigten Informationen, aktiviert sie und verarbeitet ihre Ergebnisse, bis das vorgegebene Konfidenzniveau erreicht ist. Anstatt die Dateien manuell auf jede Maschine zu kopieren, die einen Worker ausführt, werden die Dateien über die Verbindung gesendet. Maude-Inklusionen werden aufgelöst und eine abgeflachte Version der Maude-Quellen wird gesendet.
QMaude bietet Statistical Model Checking (SMC) des Modells im gleichen Formalismus.
Kopieren Sie latency.quatex und smc.maude in Ihr Experimentverzeichnis (oder behalten Sie sie in results).
Ändern Sie die erstere Datei, um das Ziel-(probabilistische)-Experiment zu laden.
Führen Sie aus```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaude gibt den erwarteten Wert für die quatex-Abfragen (μ) zurück, sowie die Anzahl der Monte-Carlo-Simulationen, die benötigt wurden, um diesen Wert zu erreichen.
## Tests
Um die Tests auszuführen, installieren Sie zunächst pytest in Ihrer Umgebung.```
pip install -e .[test]
Dann führe die Unit-Tests aus.``` python -m pytest
## Andere Dienstprogramme
Um ein Verzeichnis von Bildern in eine JSON-Metadatendatei zu konvertieren, die im Experiment verwendet wird,
Zum Beispiel, um die vom mastodon tgen client verwendeten Bilder zu generieren (ähnlich Coverbilder für destini)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
Verwenden Sie plotfinal.py mit den Argumenten 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/
Dasselbe Skript wird die CDF-Diagramme erzeugen.```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/
Die folgenden Projekte werden direkt von Maude-HCS verwendet