raytheonbbn/maude-hcsMarco de modelado y análisis formal para sistemas de comunicación ocultos, que permite la especificación de canales encubiertos, modelos adversarios y verificación estadística de modelos de las compensaciones entre indetectabilidad y rendimiento.
Maude-HCS es una de las primeras cadenas de herramientas generalizadas y modulares para especificar formalmente y razonar sobre Sistemas de Comunicación Oculta (HCS) a escalas del mundo real. Permite a los diseñadores de redes explorar diseños alternativos de HCS de forma rápida y efectiva y proporciona garantías formales de privacidad y rendimiento necesarias para confiar en el diseño.
Los sistemas de comunicación oculta (HCS) incrustan mensajes encubiertos en la actividad normal de la red para ocultar la presencia de comunicación. En la práctica, la indetectabilidad de un HCS se evalúa típicamente usando estadísticas de tráfico ad hoc o detectores específicos, lo que hace que las afirmaciones de seguridad estén estrechamente vinculadas a configuraciones experimentales y suposiciones implícitas del adversario.
Maude-HCS es un marco de modelado y análisis ejecutable que proporciona una base fundamentada y ejecutable para razonar sobre los compromisos entre indetectabilidad y rendimiento en diseños complejos de HCS. Los diseñadores especifican formalmente el comportamiento del protocolo, las observaciones del adversario y las suposiciones ambientales, y generan muestras de Monte Carlo a partir de las distribuciones de trazas inducidas. Estas pueden usarse para auditar afirmaciones de indetectabilidad estimando las tasas de verdaderos y falsos positivos de una prueba estadística y convirtiendo estas estimaciones en cotas inferiores de medidas de indetectabilidad. Esto permite la evaluación sistemática de la detectabilidad y sus compromisos con el rendimiento bajo suposiciones de modelado explícitamente establecidas.
Por favor, contáctenos si necesita ayuda para modelar y razonar sobre su HCS. Y considere citar nuestro trabajo si lo utiliza como parte de su investigación.```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} }
## Requisitos
Requiere la versión de python `3.12.4`
Cree su entorno preferido y actívelo, por ejemplo
Para pyenv```bash
pyenv install 3.12.4
pyenv local 3.12.4
Para conda```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2
Para virtual env```bash
python -m venv venv
source venv/bin/activate
Estructuramos el código fuente del repositorio para que importemos dns-formalization-maude como una dependencia (un submódulo). Creamos un fork de esta dependencia para poder rastrear nuestros cambios a la misma. Usamos sparse-checkout para evitar tener que hacer checkout de todo el código fuente de la dependencia, que incluye muchos archivos irrelevantes (como Testbed).
Para clonar el repositorio principal```shell git clone [email protected]:raytheonbbn/maude-hcs.git
La rama principal tiene el código fuente más reciente (posiblemente inestable).
Ramas/etiquetas más antiguas como `pwnd.cp1` se refieren a instantáneas estables utilizadas para producir resultados durante las evaluaciones
(por ejemplo, `pwnd.cp1` usado para el problema del desafío 1, y de manera similar `pwnd.cp2`).
Para usar una instantánea más antigua, cambia a la rama específica (ej. `pwnd.cp1`).
Configura el submódulo dns usando nuestra copia del código para poder rastrear cambios
realizados en el código fuente original, utiliza sparse-checkout para mantener solo las fuentes relevantes```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
En el comando anterior, establezca <branch> ya sea en pwnd.43.rb1 para reproducir los resultados del problema 1 del desafío,
o en pwnd para la versión más reciente.
Lo anterior debería crear un nuevo archivo llamado sparse-checkout dentro de
.git/modules/maude_hcs/deps/dns_formalization/info/
e indicarle que solo incluya ciertos directorios como Maude/src.
En este punto, git status debería mostrar un inicio limpio.
Para instalar, primero instale la dependencia como un paquete llamado dns, importamos como Maude.*
luego instale maude_hcs como un paquete (con dependencia de dns).```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## Generar modelos de usuario automáticamente
Los modelos de usuario son modelos de Markov diseñados para representar cómo se comportan los usuarios.
Estos se proporcionan en formato json.
El primer paso es convertirlos a representaciones formales en maude.
Para hacerlo, especifique
- protocolo: dns o mastodon
- directorio de entrada que contenga todos los modelos json que desea convertir
- directorio de salida que contendrá todas las versiones maude de los modelos json
Por ejemplo,```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/"
Vea ejemplos de especificaciones markov json en ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
(y de manera similar para mastodon), junto con sus especificaciones maude convertidas.
Generamos configuraciones iniciales usando el comando generate.
Las configuraciones HCS se pueden pasar directamente en json usando parámetros de configuración HCS,
o usando un archivo de configuración de experimento Shadow, o usando un archivo de configuración YML.
Cada uno de estos se describe a continuación.
Pase un archivo de configuración json de maude-hcs de la siguiente manera,
Para generar una configuración de modelo DNS probabilístico con iodine y especificar el nombre del archivo de salida,```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` para generar una versión no determinista.
Esto produce el archivo maude ejecutable (y el correspondiente archivo json de configuración HCS) en el directorio de salida.
El archivo de configuración json de entrada debería ser sencillo de seguir. Incluye la especificación de
* topología de red (enlaces y sus características)
* adversario (en este caso, perfiles de detector de zeek, datos de referencia para detectores de media móvil y sus configuraciones)
* canales/protocolos: cada protocolo incluye una red extraña y un protocolo de red subyacente. El primero oculta/incrusta datos en el segundo. Por ejemplo, Iodine se incrusta en DNS (por lo que el canal se llama iodine-dns) y Destini se incrusta en Mastodon
Consulte [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/main/HCSParamsGuide.md) para obtener una descripción de algunos de los parámetros.
Tenga en cuenta que el modelo probabilístico combinará los parámetros no deterministas así como los parámetros probabilísticos (que anulan los no deterministas).
### Usando una configuración YML
#### Configuraciones individuales
Una configuración YML contiene la configuración completa de los túneles y las redes subyacentes.
Podemos generar una configuración HCS directamente a partir de ella.```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
Para configuraciones por lotes como las de CP2, convierte múltiples archivos YML a archivos de escenario Maude:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
Donde `scenario_dir` es opcional (por defecto `../pwnd_cp2`)
### Usando configuración Shadow yaml
La configuración de red puede especificarse usando un archivo shadow en lugar de nuestro HCS config json
(Ver simulador [Shadow](https://github.com/shadow/shadow) para más información sobre especificaciones de shadow).
Para generar un modelo que use las características definidas en un archivo shadow, especifica:```shell
--shadow-filename <path_to_shadow_file.yaml>
El archivo yaml de shadow especifica las configuraciones de red, host y procesos.
Suponiendo que la configuración de red de shadow se encuentra en el directorio ../pwnd-cp1, ejecute```shell
maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow
## Ejecutar configuraciones de HCS
### Ejecución independiente con Maude
Para ejecutar una configuración en Maude independiente, primero instale [Maude independiente](https://github.com/maude-lang/Maude) para su sistema (recomendamos la versión 3.5.0 o inferior)
Para ejecutar una configuración única, invoque maude con el nombre del archivo, por ejemplo, en `results`,```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
Dentro del prompt de Maude, escribe```shell rew initConfig .
Esto ejecutará todas las reescrituras hasta que no se encuentren más reglas y no se pueda avanzar.
La adición de registro aumentará la verbosidad de la ejecución con```shell
set print attribute on .
La ejecución también se puede recorrer paso a paso con los siguientes comandos (consulte el manual de maude)```shell rew[1] initConfig . cont 1 .
### Verificación de Modelos Estadísticos
La verificación de modelos estadísticos está disponible mediante el subcomando scheck en [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 ejemplo de ejecución de SMC para el archivo generado por el comando anterior es:```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
El modelo probabilístico y su configuración inicial deben especificarse en Maude y proporcionarse mediante la opción ``--test TEST`` (por defecto: ``results/generated_test.maude``).
La ejecución de Maude comienza desde el término inicial proporcionado mediante la opción ``--initail INITIAL`` (por defecto: ``initConfig`` especificado en ``TEST``) y reescribe hasta la configuración final.
A partir de la configuración final, los observables se extraen utilizando los actores monitor y adversario especificados en el archivo fuente de Maude para el problema de verificación de modelos, proporcionado mediante la opción ``--file FILE``, o mediante la opción ``--protocol PR``.
Por ejemplo, ``--protocol dns`` hace referencia a un archivo de verificación de modelos creado específicamente para el protocolo dns bajo `lib/`.
Las propiedades cuantitativas, como el valor esperado de la latencia media, se pueden especificar mediante una fórmula QuaTEx y proporcionarse a través de la opción ``--query QUERY`` (por defecto: ``smc/query.quatex``).
Nuestros ejemplos de latencia y métricas de escalabilidad en términos de archivos exfiltrados están definidos en ``smc/latency.quatex`` y ``smc/scalability_cp2_scenario_1.quatex``, e importados en ``smc/cp2_eval_cp2_scenario_1.quatex``, y pueden expresarse con una fórmula QuaTEx de la siguiente forma:```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()];
donde la expresión Latency() extrae el valor de latencia del monitor y evalúa su expectativa con delta = 2.
La expresión ExfilFilesC2() evalúa condicionalmente el número de archivos exfiltrados:
Si el tiempo de detección basado en el número acumulativo de consultas DNS post-NAT es cero — lo que significa que no ocurre detección porque el recuento acumulativo de consultas nunca supera su umbral (por ejemplo, 416 en el ejemplo anterior) — la muestra se descarta;
de lo contrario, se evalúa el número de archivos exfiltrados hasta el momento de la detección.
El muestreo continúa hasta que se alcanza el número especificado de muestras (es decir, la opción -n min-max, como -n 30-300) o todas las consultas se responden con la significancia estadística deseada.
En el ejemplo a continuación, la segunda consulta se responde después de 30 muestras usando los valores predeterminados alpha=0.05 y delta=0.5, mientras que la primera consulta se responde después de 270 muestras usando with delta = 2, como se especificó anteriormente.
La salida incluye:
Si modificamos el valor del umbral en la fórmula de QuaTEx anterior a 500, algunas muestras se descartan.
Los resultados se informan junto con el número de muestras descartadas, y las garantías estadísticas se calculan utilizando las muestras restantes como se muestra a continuación.```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
Para reproducir los mismos experimentos dentro de la misma configuración de paralelización (es decir, el mismo valor de -j), use la opción --seed con la misma semilla aleatoria.
Por defecto o al pasar ‑1, la hora actual se utiliza como semilla.```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
### Automatización de pruebas
runexp.sh es un script de automatización que combina generación y análisis SMC. Acepta dos argumentos obligatorios:```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 es altamente paralelizable utilizando todos los núcleos de la máquina para obtener una aceleración casi lineal en el muestreo de Monte Carlo, usando la opción -j 0 como se indicó anteriormente.
QMaude permite aún más paralelismo entre máquinas mediante SMC distribuido (característica aún en pruebas activas)
Para ejecutar el SMC distribuido, debe haber uno o más workers que se inicien con
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
Las únicas opciones para el nuevo comando sworker son la dirección (-a) y el puerto (-p). Permanece a la espera de conexiones del controlador.
En el lado del controlador, se puede ejecutar un comando scheck ordinario con una opción adicional --distribute . Por ejemplo,
$ maude-hcs scheck --distribute workers.json
El archivo workers.json (también puede ser TOML o YAML) especifica la lista de workers para la simulación. Este archivo debe ser un diccionario con una clave workers que contenga una lista de valores de la forma { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } o simplemente { "workers": [ "127.0.0.1:1234" ] }. Aparte de eso, las opciones y la salida deben ser las mismas que en el comando scheck normal.
El comando scheck se conectará a los workers remotos, les pasará toda la información que necesiten, los activará y procesará sus resultados hasta que se alcance el nivel de confianza prescrito. En lugar de copiar manualmente los archivos a cada máquina que ejecuta un worker, los archivos se envían a través de la conexión. Las inclusiones de Maude se resuelven y se envía una versión aplanada de las fuentes de Maude.
QMaude ofrece verificación de modelos estadísticos (SMC) del modelo en el mismo formalismo.
Copia latency.quatex y smc.maude al directorio de tu experimento (o mantenlos en results).
Modifica el primero para cargar el experimento objetivo (probabilístico).
Ejecutar```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaude devuelve el valor esperado para las consultas quatex (μ), y el número de simulaciones de Monte Carlo que tomó para alcanzar ese valor.
## Pruebas
Para ejecutar las pruebas, primero instala pytest en tu entorno.```
pip install -e .[test]
Luego ejecuta las pruebas unitarias``` python -m pytest
## Otras utilidades
Para convertir un directorio de imágenes en un archivo de metadatos json utilizado en el experimento,
Por ejemplo, para generar las imágenes utilizadas por el cliente tgen de mastodon (imágenes de portada similares para destini)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
Utiliza plotfinal.py con los argumentos 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/
El mismo script generará los gráficos 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/
Los siguientes proyectos son directamente utilizados por Maude-HCS