Observação: alguns links mais antigos podem fazer referência ao nome anterior do projeto.
O que é isto
Um conjunto executável de testes de regressão de segurança orientados por atacantes:- Cada afirmação tem uma verificação de modelo executável em um espaço de estados finito.
- Muitas afirmações têm um modelo negativo correspondente que produz um rastreamento de contraexemplo para uma classe realista de falhas.
Onde ficam os modelos
Os modelos são mantidos em um repositório separado: vignesh07/openclaw-formal-models.Esse repositório está inacessível no momento (o GitHub retorna “Repository not found” na data desta redação). Se ele continuar indisponível para você, pergunte nos canais de mantenedores do OpenClaw qual é a localização atual antes de presumir que os modelos foram removidos.
Ressalvas
- Estes são modelos, não a implementação completa em TypeScript — é possível haver divergências entre o modelo e o código.
- Os resultados são limitados pelo espaço de estados explorado pelo TLC. Um resultado positivo não implica segurança além das premissas e dos limites modelados.
- Algumas afirmações dependem de premissas explícitas sobre o ambiente (por exemplo, implantação e entradas de configuração corretas).
Como reproduzir os resultados
Clone o repositório dos modelos e execute o TLC:Afirmações e alvos
Exposição do Gateway e configuração incorreta de Gateway aberto
Afirmação: vincular a interfaces além de local loopback sem autenticação pode possibilitar o comprometimento remoto e aumentar a exposição; um token ou uma senha bloqueia atacantes não autenticados, de acordo com as premissas do modelo.
Consulte também
docs/gateway-exposure-matrix.md no repositório dos modelos.
Pipeline de execução do Node (recurso de maior risco)
Afirmação:exec host=node exige (a) uma lista de permissões de comandos do Node junto com comandos declarados e (b) aprovação em tempo real quando configurada; no modelo, as aprovações usam tokens para impedir ataques de repetição.
Armazenamento de pareamento (controle de acesso a mensagens diretas)
Afirmação: as solicitações de pareamento respeitam o TTL e os limites de solicitações pendentes.Controle de entrada (menções e desvio por comandos de controle)
Afirmação: em contextos de grupo que exigem menção, um comando de controle não autorizado não pode contornar o controle de acesso por menção.Isolamento de roteamento e de chaves de sessão
Afirmação: mensagens diretas de remetentes distintos não são combinadas na mesma sessão, a menos que sejam explicitamente vinculadas ou configuradas dessa forma.Modelos v1++: concorrência, novas tentativas e correção de rastreamentos
Modelos posteriores que aumentam a fidelidade em relação a modos de falha do mundo real: atualizações não atômicas, novas tentativas e distribuição de mensagens.Concorrência e idempotência do armazenamento de pareamento
Afirmação: o armazenamento de pareamento aplicaMaxPending e a idempotência mesmo com intercalações — a operação de verificar e depois gravar deve ser atômica ou bloqueada, e a atualização não deve criar duplicatas. Especificamente: solicitações simultâneas não podem exceder MaxPending em um canal, e solicitações ou atualizações repetidas para o mesmo (channel, sender) não criam linhas pendentes ativas duplicadas.
Correlação e idempotência dos rastreamentos de entrada
Afirmação: a ingestão preserva a correlação dos rastreamentos durante a distribuição e é idempotente diante de novas tentativas do provedor. Quando um evento externo se transforma em várias mensagens internas, cada parte mantém a mesma identidade de rastreamento e evento; novas tentativas não causam processamento duplicado; se os IDs de eventos do provedor estiverem ausentes, a desduplicação recorre a uma chave segura (por exemplo, o ID do rastreamento) para evitar o descarte de eventos distintos.Precedência de dmScope no roteamento e identityLinks
Afirmação: o roteamento mantém as sessões de mensagens diretas isoladas por padrão e só combina sessões quando isso é explicitamente configurado, por meio da precedência de canais e dos vínculos de identidade. As substituições dedmScope específicas de cada canal prevalecem sobre os padrões globais; identityLinks combina sessões somente dentro de grupos explicitamente vinculados, não entre remetentes sem relação.