raytheonbbn/maude-hcsFramework formale di modellazione e analisi per sistemi di comunicazione nascosti, che consente la specifica di canali occulti, modelli di avversari e la verifica statistica di modelli dei compromessi tra indetectabilità e prestazioni.
Maude-HCS è una delle prime toolchain generalizzate e modulari per specificare formalmente e ragionare sui Sistemi di Comunicazione Nascosta (HCS) su scala reale. Consente ai progettisti di rete di esplorare progetti HCS alternativi in modo rapido ed efficace e fornisce garanzie formali di privacy-performance necessarie per fidarsi del progetto.
I sistemi di comunicazione nascosta (HCS) incorporano messaggi nascosti all'interno dell'attività di rete ordinaria per nascondere la presenza della comunicazione. In pratica, l'indetettabilità di un HCS viene tipicamente valutata utilizzando statistiche di traffico ad hoc o rilevatori specifici, rendendo le affermazioni sulla sicurezza strettamente legate a configurazioni sperimentali e ipotesi avversarie implicite.
Maude-HCS è un framework eseguibile di modellazione e analisi che fornisce una base ragionata ed eseguibile per ragionare sui compromessi tra indetettabilità e prestazioni in progetti HCS complessi. I progettisti specificano formalmente il comportamento del protocollo, le osservabili dell'avversario e le ipotesi ambientali, e generano campioni Monte Carlo dalle distribuzioni delle tracce indotte. Questi possono essere utilizzati per verificare le affermazioni di indetettabilità stimando i tassi di veri e falsi positivi di un test statistico e convertendo queste stime in limiti inferiori per le misure di indetettabilità. Ciò consente una valutazione sistematica della rilevabilità e dei suoi compromessi con le prestazioni in base a ipotesi di modellazione esplicitamente dichiarate.
Contattaci se hai bisogno di assistenza per modellare e ragionare sul tuo HCS. E considera di citare il nostro lavoro se lo usi come parte della tua ricerca.```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} }
## Requisiti
Richiede python versione `3.12.4`
Crea il tuo ambiente preferito e attivalo, ad esempio
Per pyenv```bash
pyenv install 3.12.4
pyenv local 3.12.4
Per conda```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2
Per ambiente virtuale```bash
python -m venv venv
source venv/bin/activate
Abbiamo strutturato il codice sorgente del repository in modo da importare dns-formalization-maude come dipendenza (un sottomodulo). Abbiamo creato un fork di questa dipendenza per poter tenere traccia delle nostre modifiche ad essa. Usiamo sparse-checkout per evitare di dover fare checkout di tutto il codice sorgente della dipendenza, che include molti file irrilevanti (come Testbed).
Per clonare il repository principale```shell git clone [email protected]:raytheonbbn/maude-hcs.git
Il ramo principale contiene la fonte più recente (possibilmente instabile).
I rami/tag più vecchi come `pwnd.cp1` si riferiscono a snapshot stabili utilizzati per produrre risultati durante le valutazioni
(ad esempio, `pwnd.cp1` usato per il problema sfida 1, e similmente `pwnd.cp2`).
Per utilizzare uno snapshot più vecchio, estrai il ramo specifico (es. `pwnd.cp1`).
Configura il sottomodulo dns usando il nostro clone del codice in modo da poter tracciare le modifiche
apportate al codice originale, usa sparse-checkout per mantenere solo le fonti rilevanti```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
Nel comando sopra imposta <branch> su pwnd.43.rb1 per riprodurre i risultati del problema della sfida 1,
o su pwnd per l'ultima versione.
Il comando sopra dovrebbe creare un nuovo file chiamato sparse-checkout in
.git/modules/maude_hcs/deps/dns_formalization/info/
e dirgli di includere solo certe directory come Maude/src.
A questo punto git status dovrebbe mostrare un avvio pulito.
Per installare, prima installa la dipendenza come pacchetto chiamato dns, che importiamo come Maude.*
quindi installa maude_hcs come pacchetto (con dipendenza da dns).```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## Genera automaticamente modelli utente
I modelli utente sono modelli di Markov progettati per rappresentare come gli utenti si comportano.
Questi sono forniti in formato JSON.
Il primo passo è convertirli in rappresentazioni formali Maude.
Per farlo, specifica
- protocollo: dns o mastodon
- directory di input contenente tutti i modelli JSON che desideri convertire
- directory di output che conterrà tutte le versioni Maude dei modelli JSON
Per esempio,```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/"
Vedi specifiche markov json di esempio in ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/ (e similmente per mastodon), insieme alle loro specifiche maude convertite.
Generiamo le configurazioni iniziali usando il comando generate.
Le configurazioni HCS possono essere passate direttamente in json usando i parametri di configurazione HCS, o usando un file di configurazione dell'esperimento Shadow, o usando un file di configurazione YML. Ciascuna di queste è descritta di seguito.
Passa un file di configurazione json maude-hcs come segue,
Per generare una configurazione del modello DNS probabilistico con iodine e specificare il nome del file di output,```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` per generare una versione non deterministica.
Questo produce il file maude eseguibile (e il corrispondente file json di configurazione HCS) nella directory di output.
Il file di configurazione json di input dovrebbe essere facile da seguire. Include la specifica di
* topologia di rete (collegamenti e loro caratteristiche)
* avversario (in questo caso profili dei rilevatori zeek, dati di base per i rilevatori a media mobile e le loro configurazioni)
* canali/protocolli: ogni protocollo include una rete weird e un protocollo di rete sottostante. Il primo nasconde/incorpora dati nel secondo. Ad esempio, Iodine si incorpora in DNS (quindi il canale si chiama iodine-dns) e Destini si incorpora in Mastodon
Fai riferimento a [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/main/HCSParamsGuide.md) per una descrizione di alcuni parametri.
Nota che il modello probabilistico combinerà i parametri non deterministici così come i parametri probabilistici (che sovrascrivono quelli non deterministici).
### Utilizzo di una configurazione YML
#### Configurazioni singole
Una configurazione YML contiene la configurazione completa dei tunnel e delle reti sottostanti.
Possiamo generare direttamente una configurazione HCS da essa.```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
Per configurazioni in batch come quelle in CP2, converti più file YML in file di scenario Maude:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
Dove `scenario_dir` è opzionale (predefinito su `../pwnd_cp2`)
### Utilizzo della configurazione yaml di Shadow
La configurazione di rete può essere specificata utilizzando un file shadow invece del nostro HCS config json
(Vedi il simulatore [Shadow](https://github.com/shadow/shadow) per maggiori informazioni sulle specifiche shadow).
Per generare un modello che utilizzi le caratteristiche definite in un file shadow, specifica:```shell
--shadow-filename <path_to_shadow_file.yaml>
Il file YAML shadow specifica le configurazioni di rete, host e processi.
Supponendo che la configurazione di rete shadow si trovi nella directory ../pwnd-cp1, esegui```shell
maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow
## Esecuzione delle configurazioni HCS
### Esecuzione standalone con Maude
Per eseguire una configurazione in maude standalone, installa prima [standalone maude](https://github.com/maude-lang/Maude) per il tuo sistema (consigliamo la versione 3.5.0 o inferiore)
Per eseguire una singola configurazione, invoca maude con il nome del file, ad esempio, in `results`,```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
All'interno del prompt di Maude, digita```shell rew initConfig .
Questo eseguirà tutte le riscritture fino a quando non verranno trovate altre regole e non si potrà fare alcun progresso.
L'aggiunta della registrazione aumenterà la verbosità dell'esecuzione con```shell
set print attribute on .
L'esecuzione può anche essere effettuata passo dopo passo con i seguenti comandi (fare riferimento al manuale di maude)```shell rew[1] initConfig . cont 1 .
### Model Checking Statistico
Il model checking statistico è disponibile tramite il sottocomando scheck in [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 esempio di esecuzione SMC per il file generato dal comando sopra è:```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
Il modello probabilistico e la sua configurazione iniziale devono essere specificati in Maude e forniti tramite l'opzione ``--test TEST`` (predefinita: ``results/generated_test.maude``).
L'esecuzione di Maude parte dal termine iniziale fornito tramite l'opzione ``--initail INITIAL`` (predefinita: ``initConfig`` specificata in ``TEST``) e riscrive fino alla configurazione finale.
Dalla configurazione finale, gli osservabili vengono estratti utilizzando gli attori monitor e adversary specificati nel file sorgente Maude per il problema di model checking, fornito tramite l'opzione ``--file FILE`` o dall'opzione ``--protocol PR``.
Ad esempio ``--protocol dns`` si riferisce a un file di model checking creato appositamente per il protocollo dns in `lib/`.
Le proprietà quantitative, come il valore atteso della latenza media, possono essere specificate utilizzando una formula QuaTEx e fornite tramite l'opzione ``--query QUERY`` (predefinita: ``smc/query.quatex``).
I nostri esempi di metriche di latenza e scalabilità in termini di file esfiltrati sono definiti in ``smc/latency.quatex`` e ``smc/scalability_cp2_scenario_1.quatex``, e importati in ``smc/cp2_eval_cp2_scenario_1.quatex``, e possono essere espressi con una formula QuaTEx della forma seguente:```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()];
where the expression Latency() estrae il valore di latenza dal monitor e ne valuta l'aspettativa con delta = 2.
L'espressione ExfilFilesC2() valuta condizionalmente il numero di file esfiltrati:
Se il tempo di rilevamento basato sul numero cumulativo di query DNS post-NAT è zero - il che significa che non si verifica alcuna rilevazione perché il conteggio cumulativo delle query non supera mai la sua soglia (ad esempio, 416 nell'esempio sopra) - il campione viene scartato;
altrimenti, viene valutato il numero di file esfiltrati fino al momento della rilevazione.
Il campionamento continua fino a quando viene raggiunto il numero specificato di campioni (cioè l'opzione -n min-max, come -n 30-300) o tutte le query sono state risposte con la significatività statistica desiderata.
Nell'esempio seguente, la seconda query viene risolta dopo 30 campioni utilizzando i valori predefiniti alpha=0.05 e delta=0.5, mentre la prima query viene risolta dopo 270 campioni utilizzando with delta = 2, come specificato sopra.
L'output include:
Se modifichiamo il valore di soglia nella formula QuaTEx di cui sopra a 500, alcuni campioni vengono scartati.
I risultati vengono quindi riportati insieme al numero di campioni scartati, e le garanzie statistiche vengono calcolate utilizzando i campioni rimanenti, come mostrato di seguito.```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
Per riprodurre gli stessi esperimenti nella stessa impostazione di parallelizzazione (cioè lo stesso valore di -j), usa l'opzione --seed con lo stesso seme casuale.
Per impostazione predefinita oppure quando si passa ‑1, viene utilizzato il tempo corrente come seme.```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
### Automazione dei test
runexp.sh è uno script di automazione che combina generazione e analisi SMC. Prende due argomenti obbligatori:```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 è altamente parallelizzabile utilizzando tutti i core della macchina per ottenere un'accelerazione quasi lineare nel campionamento Monte Carlo, usando l'opzione -j 0 come indicato sopra. QMaude consente un parallelismo ancora maggiore tra macchine utilizzando SMC distribuito (funzionalità ancora in fase di test attivo)
Per eseguire l'SMC distribuito, devono essere avviati uno o più worker con
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
Le uniche opzioni per il nuovo comando sworker sono l'indirizzo (-a) e la porta (-p). Rimane in attesa di connessioni dal controller.
Sul lato controller, un normale comando scheck può essere eseguito con un'opzione aggiuntiva --distribute . Per esempio,
$ maude-hcs scheck --distribute workers.json
Il file workers.json (può anche essere TOML o YAML) specifica la lista dei worker per la simulazione. Questo file deve essere un dizionario con una chiave workers contenente una lista di valori della forma { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } o semplicemente { "workers": [ "127.0.0.1:1234" ] }. Per il resto, le opzioni e l'output dovrebbero essere gli stessi del normale comando scheck.
Il comando scheck si connetterà ai worker remoti, passerà loro tutte le informazioni necessarie, li attiverà e elaborerà i loro risultati fino al raggiungimento del livello di confidenza prescritto. Invece di copiare manualmente i file su ogni macchina che esegue un worker, i file vengono inviati tramite la connessione. Le inclusioni di Maude vengono risolte e viene inviata una versione appiattita delle sorgenti Maude.
QMaude offre Statistical Model Checking (SMC) del modello nello stesso formalismo.
Copia latency.quatex e smc.maude nella directory del tuo esperimento (o tienili in results).
Modifica il primo per caricare l'esperimento target (probabilistico).
Esegui```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaude restituisce il valore atteso per le query quatex (μ), e il numero di simulazioni Monte Carlo necessarie per raggiungere quel valore.
## Test
Per eseguire i test, installa prima pytest nel tuo ambiente.```
pip install -e .[test]
Quindi esegui i test unitari``` python -m pytest
## Altre utility
Per convertire una directory di immagini in un file di metadati json utilizzato nell'esperimento,
Per esempio per generare le immagini utilizzate dal client mastodon tgen (allo stesso modo cover images per destini)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
Usa plotfinal.py con gli argomenti 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/
Lo stesso script genererà i CDF plots.```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/
I seguenti progetti sono utilizzati direttamente da Maude-HCS