Verificação formal (modelos de segurança)

Os modelos formais de segurança do OpenClaw (atualmente TLA+/TLC) fornecem um argumento verificado por máquina de que caminhos específicos de maior risco — autorização, isolamento de sessões, controle de acesso a ferramentas e segurança contra configurações incorretas — aplicam a política pretendida, sob premissas explicitamente declaradas.

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.

Isto não é uma prova de que o OpenClaw seja seguro em todos os aspectos e não verifica toda a implementação em TypeScript.

Onde ficam os modelos

Os modelos são mantidos em um repositório separado: vignesh07/openclaw-formal-models.

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:

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Java 11+ required (TLC runs on the JVM).# The repo vendors a pinned tla2tools.jar and provides bin/tlc plus Make targets. make <target>

Ainda não há integração de CI com este repositório; uma iteração futura poderia adicionar modelos executados pela CI com artefatos públicos (rastreamentos de contraexemplos e logs de execução) ou um fluxo hospedado de "executar este modelo" para verificações pequenas e limitadas.

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 aplica MaxPending 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 de dmScope 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.

Relacionado

• Modelo de ameaças
• Como contribuir para o modelo de ameaças
• Resposta a incidentes