Maude-HCS

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.

Introducción

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

Install: desde el código fuente de git

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.

Generar automáticamente configuraciones HCS

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.

Usando configuración json HCS

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