Maude-HCS

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.

Einleitung

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

Install: von der Git-Quelle

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.

HCS-Konfigurationen automatisch generieren

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.

Verwendung der HCS-JSON-Konfiguration

Ü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/main/HCSParamsGuide.md).
Beachten Sie, dass das probabilistische Modell die nichtdeterministischen sowie die probabilistischen Parameter kombiniert (welche die nichtdeterministischen überschreiben).