raytheonbbn/maude-hcsEstrutura de modelagem formal e análise para sistemas de comunicação oculta, permitindo especificação de canais secretos, modelos de adversários e verificação estatística de modelos dos compromissos entre indetectabilidade e desempenho.
Maude-HCS é uma das primeiras cadeias de ferramentas generalizadas e modulares para especificar formalmente e raciocinar sobre Sistemas de Comunicação Oculta (HCS) em escalas do mundo real. Ela permite que projetistas de redes explorem rapidamente e de forma eficaz designs alternativos de HCS e fornece garantias formais de privacidade-desempenho necessárias para confiar no design.
Sistemas de comunicação oculta (HCS) embedem mensagens encobertas dentro da atividade de rede comum para ocultar a presença da comunicação. Na prática, a indetectabilidade de um HCS é tipicamente avaliada usando estatísticas de tráfego ad hoc ou detectores específicos, tornando as afirmações de segurança fortemente acopladas a configurações experimentais e suposições adversárias implícitas.
Maude-HCS é um framework de modelagem e análise executável que fornece uma base fundamentada e executável para raciocinar sobre tradeoffs de indetectabilidade–desempenho em designs complexos de HCS. Projetistas especificam formalmente o comportamento do protocolo, observáveis do adversário e suposições ambientais, e geram amostras de Monte Carlo a partir das distribuições de traços induzidas. Estas podem ser usadas para auditar afirmações de indetectabilidade estimando as taxas de verdadeiros e falsos positivos de um teste estatístico e convertendo essas estimativas em limites inferiores de medidas de indetectabilidade. Isso permite a avaliação sistemática da detectabilidade e seus tradeoffs com o desempenho sob suposições de modelagem explicitamente declaradas.
Por favor, entre em contato conosco se precisar de ajuda para modelar e raciocinar sobre seu HCS. E considere citar nosso trabalho se o utilizar como parte de sua pesquisa.```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} }
## Requirements
Requires python version `3.12.4`
Create your preferred environment and activate it, for example
For 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 ambiente virtual```bash
python -m venv venv
source venv/bin/activate
Estruturamos o código-fonte do repositório de forma que importamos dns-formalization-maude como uma dependência (um submódulo). Criamos um fork dessa dependência para podermos rastrear nossas alterações nela. Usamos sparse-checkout para evitar a necessidade de fazer checkout de todo o código-fonte da dependência, que inclui muitos arquivos irrelevantes (como Testbed).
Para clonar o repositório principal```shell git clone [email protected]:raytheonbbn/maude-hcs.git
O branch principal contém a fonte mais recente (possivelmente instável).
Ramos/etiquetas mais antigos como `pwnd.cp1` referem-se a snapshots estáveis usados para produzir resultados durante avaliações
(por exemplo, `pwnd.cp1` usado para o problema de desafio 1, e similarmente `pwnd.cp2`).
Para usar um snapshot mais antigo, faça checkout do branch específico (ex: `pwnd.cp1`).
Configure o submódulo dns usando nosso clone do código para que possamos rastrear alterações
feitas na fonte original, use sparse-checkout para manter apenas as fontes 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
No comando acima, defina <branch> como pwnd.43.rb1 para reproduzir os resultados do problema 1 do desafio, ou como pwnd para a versão mais recente.
O comando acima deve criar um novo arquivo chamado sparse-checkout em
.git/modules/maude_hcs/deps/dns_formalization/info/
e instruí-lo a incluir apenas certos diretórios, como Maude/src.
Neste ponto, git status deve mostrar um início limpo.
Para instalar, primeiro instale a dependência como um pacote chamado dns, que importamos como Maude.*, e depois instale o maude_hcs como um pacote (com dependência em dns).```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## Geração automática de modelos de usuário
Modelos de usuário são modelos markovianos destinados a representar como os usuários se comportam.
Eles são fornecidos no formato json.
O primeiro passo é convertê-los para representações formais em maude.
Para fazer isso, especifique o
- protocolo: dns ou mastodon
- diretório de entrada contendo todos os modelos json que você deseja converter
- diretório de saída que conterá todas as versões maude dos modelos json
Por exemplo,```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/"
Veja exemplos de especificações json markov em ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/ (e similarmente para mastodon), juntamente com suas especificações maude convertidas.
Geramos configurações iniciais usando o comando generate.
As configurações HCS podem ser passadas diretamente em json usando parâmetros de configuração HCS, ou usando um arquivo de configuração de experimento Shadow, ou usando um arquivo de configuração YML. Cada um destes é descrito a seguir.
Passe um arquivo de configuração json maude-hcs da seguinte forma,
Para gerar uma configuração de modelo DNS probabilístico com iodine e especificar o nome do arquivo de saída,```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/"
Defina `--model=nondet` para gerar uma versão não determinística.
Isso produz o arquivo maude executável (e o correspondente json de configuração HCS) no diretório de saída.
O arquivo de configuração json de entrada deve ser direto de seguir. Ele inclui especificação de
* topologia de rede (links e suas características)
* adversário (neste caso, perfis de detector zeek, dados de linha de base para detectores de média móvel e suas configurações)
* canais/protocolos: cada protocolo inclui uma rede estranha e um protocolo de rede subjacente. O primeiro oculta/incorpora dados no segundo. Por exemplo, Iodine incorpora em DNS (então o canal é chamado iodine-dns) e Destini incorpora em Mastodon
Consulte [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/HEAD/HCSParamsGuide.md) para uma descrição de alguns dos parâmetros.
Note que o modelo probabilístico combinará os parâmetros não determinísticos, bem como os parâmetros probabilísticos (que substituem os não determinísticos).
### Usando uma configuração YML
#### Configurações únicas
Uma configuração YML contém a configuração completa dos túneis e redes subjacentes.
Podemos gerar uma configuração HCS diretamente a partir dela.```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
Para configurações em lote como as do CP2, converta vários arquivos YML em arquivos de cenário Maude:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
Onde `scenario_dir` é opcional (padrão é `../pwnd_cp2`)
### Usando configuração yaml do Shadow
A configuração de rede pode ser especificada usando um arquivo shadow em vez do nosso json de configuração HCS
(Veja o simulador [Shadow](https://github.com/shadow/shadow) para mais informações sobre especificações shadow).
Para gerar um modelo que usa características definidas em um arquivo shadow, especifique:```shell
--shadow-filename <path_to_shadow_file.yaml>
O arquivo shadow yaml especifica as configurações de rede, host e processos.
Assumindo que a configuração de rede shadow está localizada no diretório ../pwnd-cp1, execute```shell
maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow
## Executar Configurações HCS
### Execução standalone com Maude
Para executar uma configuração no maude standalone, primeiro instale o [maude standalone](https://github.com/maude-lang/Maude) para o seu sistema (recomendamos a versão 3.5.0 ou inferior)
Para executar uma única configuração, invoque o maude com o nome do arquivo, por exemplo, em `results`,```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
Dentro do prompt do Maude, digite```shell rew initConfig .
Isso executará todas as reescritas até que não sejam encontradas mais regras e nenhum progresso possa ser feito.
A adição de logging aumentará a verbosidade da execução com```shell
set print attribute on .
A execução também pode ser percorrida passo a passo com os seguintes comandos (consulte o manual do Maude)```shell rew[1] initConfig . cont 1 .
### Verificação Estatística de Modelos
Verificação estatística de modelos está disponível por meio do subcomando scheck no [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.
Um exemplo de execução SMC para o arquivo gerado pelo comando acima é:```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
O modelo probabilístico e sua configuração inicial devem ser especificados em Maude e fornecidos via a opção ``--test TEST`` (padrão: ``results/generated_test.maude``).
A execução Maude começa a partir do termo inicial fornecido via a opção ``--initail INITIAL`` (padrão: ``initConfig`` especificado em ``TEST``) e reescreve até a configuração final.
A partir da configuração final, os observáveis são extraídos usando os atores monitor e adversário especificados no arquivo fonte Maude para o problema de verificação de modelo, fornecido via opção ``--file FILE``, ou pela opção ``--protocol PR``.
Por exemplo ``--protocol dns`` refere-se a um arquivo de verificação de modelo criado especificamente para o protocolo dns em `lib/`.
Propriedades quantitativas, como o valor esperado da latência média, podem ser especificadas usando uma fórmula QuaTEx e fornecidas via opção ``--query QUERY`` (padrão: ``smc/query.quatex``).
Nossas métricas de exemplo de latência e escalabilidade em termos de arquivos exfiltrados são definidas em ``smc/latency.quatex`` e ``smc/scalability_cp2_scenario_1.quatex``, e importadas para ``smc/cp2_eval_cp2_scenario_1.quatex``, e podem ser expressas com uma fórmula QuaTEx da seguinte 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()];
onde a expressão Latency() extrai o valor de latência do monitor e avalia sua expectativa com delta = 2.
A expressão ExfilFilesC2() avalia condicionalmente o número de arquivos exfiltrados:
Se o tempo de detecção baseado no número cumulativo de consultas DNS pós-NAT for zero - significando que nenhuma detecção ocorre porque a contagem cumulativa de consultas nunca excede seu limite (por exemplo, 416 no exemplo acima) - a amostra é descartada;
caso contrário, o número de arquivos exfiltrados até o momento da detecção é avaliado.
A amostragem continua até que o número especificado de amostras seja atingido (ou seja, opção -n min-max, como -n 30-300) ou todas as consultas sejam respondidas com a significância estatística desejada.
No exemplo abaixo, a segunda consulta é respondida após 30 amostras usando os valores padrão alpha=0.05 e delta=0.5, enquanto a primeira consulta é respondida após 270 amostras usando com delta = 2, conforme especificado acima.
A saída inclui:
Se modificarmos o valor limite na fórmula QuaTEx acima para 500, algumas amostras são descartadas.
Os resultados são então reportados juntamente com o número de amostras descartadas, e as garantias estatísticas são calculadas usando as amostras restantes conforme mostrado abaixo.```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 reproduzir os mesmos experimentos dentro da mesma configuração de paralelização (ou seja, o mesmo valor de -j), use a opção --seed com a mesma semente aleatória.
Por padrão ou ao passar ‑1, o tempo atual é usado como semente.```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
### Automação de testes
runexp.sh é um script de automação que combina geração e análise SMC. Requer dois argumentos obrigatórios:```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
O SMC é altamente paralelizável usando todos os núcleos da máquina para obter aceleração quase linear na amostragem de Monte Carlo, utilizando a opção -j 0 conforme indicado acima.
O QMaude permite ainda mais paralelismo entre máquinas usando SMC distribuída (funcionalidade ainda em teste ativo).
Para executar a SMC distribuída, deve haver um ou mais workers que são iniciados com
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 Listening on 127.0.0.1:1234...
As únicas opções para o novo comando sworker são o endereço (-a) e a porta (-p). Ele fica aguardando conexões do controlador.
No lado do controlador, um comando scheck comum pode ser executado com uma opção adicional --distribute . Por exemplo,
$ maude-hcs scheck --distribute workers.json
O arquivo workers.json (também pode ser TOML ou YAML) especifica a lista de workers para a simulação. Este arquivo deve ser um dicionário com uma chave workers contendo uma lista de valores da forma { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } ou simplesmente { "workers": [ "127.0.0.1:1234" ] }. Fora isso, as opções e a saída devem ser as mesmas do comando scheck regular.
O comando scheck irá conectar-se aos workers remotos, passar a eles todas as informações necessárias, ativá-los e processar seus resultados até que o nível de confiança prescrito seja alcançado. Em vez de copiar manualmente os arquivos para cada máquina que executa um worker, os arquivos são enviados através da conexão. As inclusões do Maude são resolvidas e uma versão simplificada dos fontes do Maude é enviada.
O QMaude oferece Verificação Estatística de Modelos (SMC) do modelo no mesmo formalismo.
Copie latency.quatex e smc.maude para o diretório do seu experimento (ou mantenha-os em results).
Modifique o primeiro para carregar o experimento alvo (probabilístico).
Execute```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaude retorna o valor esperado para as consultas quatex (μ) e o número de simulações de Monte Carlo que foram necessárias para atingir esse valor.
## Testes
Para executar os testes, instale primeiro o pytest no seu ambiente.```
pip install -e .[test]
Em seguida, execute os testes unitários``` python -m pytest
## Outros utilitários
Para converter um diretório de imagens em um arquivo de metadados json usado no experimento,
Por exemplo, para gerar as imagens usadas pelo cliente mastodon tgen (similarmente, imagens de capa para destini)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
Use plotfinal.py com os 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/
O mesmo script gerará os 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/
Os seguintes projetos são diretamente utilizados pelo Maude-HCS