Maude-HCS

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.

Introdução

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

Instalação: a partir da fonte git

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.

Gerar automaticamente configurações HCS

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.

Usando Configuração json HCS

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