Verificação Formal (Modelos de Segurança)

Esta página rastreia os modelos de segurança formais do Mayros (TLA+/TLC hoje; mais conforme necessário).

Nota: alguns links antigos podem se referir ao nome anterior do projeto.

Objetivo (estrela norte): fornecer um argumento verificado por máquina de que o Mayros aplica sua política de segurança pretendida (autorização, isolamento de sessão, controle de ferramenta e segurança contra configuração incorreta), sob suposições explícitas.

O que isso é (hoje): uma suíte de regressão de segurança executável e orientada a atacante:

  • Cada afirmação tem uma verificação de modelo executável sobre um espaço de estado finito.
  • Muitas afirmações têm um modelo negativo pareado que produz um trace de contraexemplo para uma classe de bug realista.

O que isso não é (ainda): uma prova de que "Mayros é seguro em todos os aspectos" ou que a implementação completa em TypeScript está correta.

Onde os modelos ficam

Modelos são mantidos em um repositório separado: vignesh07/mayros-formal-models.

Avisos importantes

  • Estes são modelos, não a implementação completa em TypeScript. Deriva entre modelo e código é possível.
  • Resultados são limitados pelo espaço de estado explorado pelo TLC; "verde" não implica segurança além das suposições e limites modelados.
  • Algumas afirmações dependem de suposições ambientais explícitas (por exemplo, implantação correta, entradas de configuração corretas).

Reproduzindo resultados

Hoje, resultados são reproduzidos clonando o repositório de modelos localmente e executando TLC (veja abaixo). Uma iteração futura poderia oferecer:

  • Modelos executados em CI com artefatos públicos (traces de contraexemplo, logs de execução)
  • um fluxo de trabalho hospedado "executar este modelo" para verificações pequenas e limitadas

Começando:

bash
git clone https://github.com/vignesh07/mayros-formal-models
cd mayros-formal-models

# Java 11+ necessário (TLC executa na JVM).
# O repositório inclui um `tla2tools.jar` fixado (ferramentas TLA+) e fornece `bin/tlc` + alvos Make.

make <target>

Exposição do Gateway e configuração incorreta de gateway aberto

Afirmação: vinculação além de loopback sem autenticação pode tornar comprometimento remoto possível / aumenta exposição; token/senha bloqueia atacantes não autorizados (conforme as suposições do modelo).

  • Execuções verdes:
    • make gateway-exposure-v2
    • make gateway-exposure-v2-protected
  • Vermelho (esperado):
    • make gateway-exposure-v2-negative

Veja também: docs/gateway-exposure-matrix.md no repositório de modelos.

Pipeline Nodes.run (capacidade de maior risco)

Afirmação: nodes.run requer (a) lista de permissões de comando de node mais comandos declarados e (b) aprovação ao vivo quando configurado; aprovações são tokenizadas para prevenir replay (no modelo).

  • Execuções verdes:
    • make nodes-pipeline
    • make approvals-token
  • Vermelho (esperado):
    • make nodes-pipeline-negative
    • make approvals-token-negative

Armazenamento de pareamento (controle de DM)

Afirmação: solicitações de pareamento respeitam TTL e limites de solicitações pendentes.

  • Execuções verdes:
    • make pairing
    • make pairing-cap
  • Vermelho (esperado):
    • make pairing-negative
    • make pairing-cap-negative

Controle de ingresso (menções + bypass de comando de controle)

Afirmação: em contextos de grupo que requerem menção, um "comando de controle" não autorizado não pode contornar o controle de menção.

  • Verde:
    • make ingress-gating
  • Vermelho (esperado):
    • make ingress-gating-negative

Isolamento de roteamento/chave de sessão

Afirmação: DMs de pares distintos não entram em colapso na mesma sessão a menos que explicitamente vinculados/configurados.

  • Verde:
    • make routing-isolation
  • Vermelho (esperado):
    • make routing-isolation-negative

v1++: modelos limitados adicionais (concorrência, tentativas, corretude de trace)

Estes são modelos de acompanhamento que aumentam a fidelidade em torno de modos de falha do mundo real (atualizações não atômicas, tentativas e distribuição de mensagens).

Concorrência / idempotência de armazenamento de pareamento

Afirmação: um armazenamento de pareamento deve aplicar MaxPending e idempotência mesmo sob intercalações (ou seja, "check-then-write" deve ser atômico / bloqueado; refresh não deve criar duplicatas).

O que significa:

  • Sob solicitações concorrentes, você não pode exceder MaxPending para um canal.

  • Solicitações/refreshes repetidos para o mesmo (channel, sender) não devem criar linhas pendentes ativas duplicadas.

  • Execuções verdes:

    • make pairing-race (verificação de limite atômico/bloqueado)
    • make pairing-idempotency
    • make pairing-refresh
    • make pairing-refresh-race

  • Vermelho (esperado):

    • make pairing-race-negative (corrida de limite begin/commit não atômico)
    • make pairing-idempotency-negative
    • make pairing-refresh-negative
    • make pairing-refresh-race-negative

Correlação / idempotência de trace de ingresso

Afirmação: a ingestão deve preservar correlação de trace através de distribuição e ser idempotente sob tentativas de provedor.

O que significa:

  • Quando um evento externo se torna múltiplas mensagens internas, cada parte mantém a mesma identidade de trace/evento.

  • Tentativas não resultam em processamento duplo.

  • Se IDs de evento de provedor estiverem faltando, dedupe retorna a uma chave segura (por exemplo, ID de trace) para evitar descartar eventos distintos.

  • Verde:

    • make ingress-trace
    • make ingress-trace2
    • make ingress-idempotency
    • make ingress-dedupe-fallback

  • Vermelho (esperado):

    • make ingress-trace-negative
    • make ingress-trace2-negative
    • make ingress-idempotency-negative
    • make ingress-dedupe-fallback-negative

Precedência de dmScope de roteamento + identityLinks

Afirmação: o roteamento deve manter sessões DM isoladas por padrão, e apenas colapsar sessões quando explicitamente configurado (precedência de canal + links de identidade).

O que significa:

  • Substituições de dmScope específicas de canal devem vencer sobre padrões globais.

  • identityLinks devem colapsar apenas dentro de grupos vinculados explícitos, não através de pares não relacionados.

  • Verde:

    • make routing-precedence
    • make routing-identitylinks

  • Vermelho (esperado):

    • make routing-precedence-negative
    • make routing-identitylinks-negative