Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems

Título: Maude-HCS: Verificação de Modelos das Compensações entre Indetectabilidade e Desempenho em Sistemas de Comunicação Oculta

1. O Problema

Os Sistemas de Comunicação Oculta (HCS - Hidden Communication Systems) têm como objetivo embutir mensagens secretas em atividades de rede normais, ocultando não apenas o conteúdo, mas a própria existência da comunicação. Essas ferramentas são vitais para liberdade na internet e segurança nacional (ex.: jornalistas e militares em regimes autoritários).

No entanto, a avaliação atual da indetectabilidade desses sistemas é frequentemente:

• Ad hoc: Baseada em estatísticas de tráfego específicas ou detectores manuais.
• Não escalável: Depende de simulações e experimentos em testbeds físicos, o que é rígido, propenso a erros e consome muito tempo.
• Falta de formalismo: Não existe uma estrutura geral para modelar formalmente as propriedades de desempenho e indetectabilidade, tornando difícil explorar o espaço de design, evoluir o sistema ou comparar diferentes abordagens de forma rigorosa.

O desafio central é quantificar o compromisso (tradeoff) entre o desempenho (ex.: taxa de transferência, latência) e o risco de detecção por um adversário, sob suposições explícitas.

2. Metodologia

Os autores apresentam o Maude-HCS, uma ferramenta de modelagem e análise executável baseada em lógica de reescrita (rewriting logic). A metodologia segue os seguintes pilares:

• Fundação Formal (Maude e PMaude):

  • Utiliza a linguagem Maude e sua extensão probabilística PMaude, que permite especificar sistemas distribuídos com tempo real e probabilidades.
  • Modela o sistema como uma teoria de reescrita de atores generalizados, onde estados são multiconjuntos de objetos e mensagens, e transições são regras de reescrita.
  • Transforma modelos não determinísticos em modelos probabilísticos executáveis através de transformações automáticas ($P$, $Sim$, $M$), permitindo a remoção de não determinismos para análise estatística.

• Definição Formal de Indetectabilidade:

  • A indetectabilidade é definida como a indistinguibilidade estatística entre as distribuições de traços de execução observáveis de dois mundos:
    1. Ord: O sistema baseline sem comunicação oculta.
    2. HCS: O sistema com tráfego oculto embutido.
  • Formalmente, um sistema é $(M, d)$-indetectável se a medida de divergência $M$ (ex.: Divergência de Kullback-Leibler - KL) entre as distribuições de traços $View_{Ord}$ e $View_{HCS}$ for menor que um limite $d$.

• Auditoria via Verificação de Modelo Estatístico (SMC):

  • Em vez de estimar distribuições completas (o que é computacionalmente inviável devido à alta dimensionalidade), o Maude-HCS utiliza Verificação de Modelo Estatístico (SMC) com simulações de Monte Carlo.
  • Método de Auditoria:
    1. Gera amostras de traços observáveis para ambos os mundos (Ord e HCS).
    2. Executa um detector adversário $\phi$ (classificador binário) sobre essas amostras.
    3. Calcula a Taxa de Verdadeiros Positivos (TPR) e a Taxa de Falsos Positivos (FPR).
    4. Usa a desigualdade de processamento de dados da Divergência KL para derivar um limite inferior certificado para a indetectabilidade:
       $$D_{KL}(Q_t \| P_t) \geq D_{KL}(\text{Bern}(TPR) \| \text{Bern}(FPR))$$
  • Se o limite inferior calculado exceder o parâmetro de privacidade alegado, a afirmação de indetectabilidade é falsificada sob as suposições do modelo.

• Fluxo de Trabalho Modular:

  • Os designers especificam o protocolo de rede base e aplicam "padrões formais" (ex.: tunneling) para criar o sistema "estranho" (weird network) que contém a comunicação oculta.
  • O sistema é instrumentado com monitores para coletar métricas de desempenho (latência, goodput) e observáveis do adversário.

3. Principais Contribuições

1. Formalização da Indetectabilidade: Define a indetectabilidade como uma condição quantitativa de indistinguibilidade entre distribuições de traços observáveis, expressa através de limites em medidas de divergência (como KL).
2. Modelos Semânticos Alinhados e Escaláveis: Integra técnicas de ponta para reduzir a carga de modelagem, transformando automaticamente modelos não determinísticos em probabilísticos, garantindo consistência semântica entre o modelo e a análise.
3. Metodologia de Auditoria: Introduz um método para auditar afirmações de privacidade usando SMC, permitindo que designers estimem TPR/FPR e convertam isso em limites inferiores rigorosos para medidas de indetectabilidade.
4. Exploração Sistemática de Espaços de Design: Demonstra a capacidade de varrer parâmetros de implantação (perda de rede, tráfego de fundo, configurações de protocolo) para mapear o espaço de compromissos entre desempenho e risco de detecção.

4. Resultados e Avaliação

Os autores avaliaram o Maude-HCS em uma implementação de prova de conceito baseada em tunneling (Iodine sobre DNS e Destini sobre Mastodon) e validaram os resultados contra um testbed físico real.

• Análise de Compensação (Trade-off):

  • Em diferentes cenários (variação de perda de pacotes e tráfego de fundo), o aumento do desempenho (redução do tempo de espera entre envios) geralmente aumentou a distinguibilidade estatística (maior Divergência KL), tornando o sistema mais detectável.
  • A ferramenta permitiu identificar pontos de operação onde o sistema permanece indetectável sob limites específicos, mesmo com alta taxa de transferência.

• Validação Semântica (Alinhamento Modelo-Realidade):

  • Comparação entre as previsões do modelo Maude e os dados do testbed físico mostrou um forte alinhamento.
  • Para métricas de latência e goodput, os resultados do modelo caíram dentro de um desvio padrão dos dados experimentais (diferença máxima de ~13,6% em latência e ~17,1% em goodput).
  • A Divergência KL entre as distribuições de latência do modelo e do experimento foi próxima de zero, indicando que o modelo captura fielmente o comportamento do sistema real, incluindo bugs e peculiaridades de implementação.

• Auditoria de Detectores:

  • O sistema foi capaz de auditar múltiplos detectores (contagem de consultas DNS, contagem de requisições HTTPS, médias móveis) e mostrar como a alteração de limiares (thresholds) afeta drasticamente a evidência de divergência e a probabilidade de detecção.

5. Significado e Conclusão

O trabalho do Maude-HCS representa um avanço significativo na segurança de redes e na análise de sistemas de comunicação oculta:

• Mudança de Paradigma: Transita da avaliação empírica e ad hoc para uma abordagem formal, baseada em modelos e auditável.
• Confiança no Design: Permite que designers de HCS validem garantias de privacidade e desempenho antes da implementação física, reduzindo o risco de falhas críticas em ambientes de alta ameaça.
• Reprodutibilidade e Rigor: Oferece uma linguagem precisa para declarar e verificar afirmações de indetectabilidade, tornando explícitas as suposições sobre o adversário e o ambiente.
• Futuro: Os autores sugerem que o próximo passo é inverter o processo: projetar novos sistemas de comunicação oculta diretamente a partir do modelo formal Maude-HCS e gerar implementações de código corretas por construção (correct-by-construction), eliminando a lacuna entre a teoria e a prática.

Em resumo, o Maude-HCS fornece a primeira ferramenta generalizada para especificar e raciocinar formalmente sobre sistemas de comunicação oculta em escala real, permitindo uma exploração sistemática e confiável dos compromissos entre desempenho e segurança.