Verificación Formal (Modelos de Seguridad)

Esta página rastrea los **modelos de seguridad formales** de OpenClaw (TLA+/TLC hoy; más según sea necesario).

**Objetivo (estrella guía):** proporcionar un argumento verificado por máquina de que OpenClaw hace cumplir su

política de seguridad prevista (autorización, aislamiento de sesión, gating de herramientas, y

seguridad contra mala configuración), bajo supuestos explícitos.

**Lo que esto es (hoy):** un **suite de regresión de seguridad** ejecutable y dirigido por atacante:

- Cada afirmación tiene un model-check ejecutable sobre un espacio de estados finito.

- Muchas afirmaciones tienen un **modelo negativo** emparejado que produce una traza de contraejemplo para una clase de bug realista.

**Lo que esto no es (aún):** una prueba de que "OpenClaw es seguro en todos los aspectos" o que la implementación completa en TypeScript es correcta.

Los modelos se mantienen en un repo separado: ''vignesh07/openclaw-formal-models''.

- Estos son **modelos**, no la implementación completa en TypeScript. Es posible que haya deriva entre modelo y código.

- Los resultados están limitados por el espacio de estados explorado por TLC; "verde" no implica seguridad más allá de los supuestos y límites modelados.

- Algunas afirmaciones dependen de supuestos ambientales explícitos (ej., despliegue correcto, entradas de configuración correctas).

Hoy, los resultados se reproducen clonando el repo de modelos localmente y ejecutando TLC (ver abajo). Una iteración futura podría ofrecer:

- Modelos ejecutados en CI con artefactos públicos (trazas de contraejemplo, logs de ejecución)

- un flujo de trabajo hospedado "ejecutar este modelo" para verificaciones pequeñas y limitadas

Para empezar:

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

make '<target>'

**Afirmación:** vincular más allá de loopback sin auth puede hacer posible el compromiso remoto / aumenta la exposición; token/bloquea atacantes no autenticados (según los supuestos del modelo).

- Ejecuciones verdes:

- ''make gateway-exposure-v2''

- ''make gateway-exposure-v2-protected''

- Rojo (esperado):

- ''make gateway-exposure-v2-negative''

Ver también: ''docs/gateway-exposure-matrix.md'' en el repo de modelos.

**Claim:** ''nodes.run'' requires (a) node command allowlist plus declared commands and (b) live approval when configured; approvals are tokenized to prevent replay (in the model).

- Green runs:

- ''make nodes-pipeline''

- ''make approvals-token''

- Red (expected):

- ''make nodes-pipeline-negative''

- ''make approvals-token-negative''

**Claim:** pairing requests respect TTL and pending-request caps.

- Green runs:

- ''make pairing''

- ''make pairing-cap''

- Red (expected):

- ''make pairing-negative''

- ''make pairing-cap-negative''

**Afirmación:** en contextos de grupo que requieren mención, un "comando de control" no autorizado no puede evitar el gating de mención.

- Verde:

- ''make ingress-gating''

- Rojo (esperado):

- ''make ingress-gating-negative''

**Afirmación:** DMs de pares distintos no colapsan en la misma sesión a menos que estén explícitamente vinculados/configurados.

- Verde:

- ''make routing-isolation''

- Rojo (esperado):

- ''make routing-isolation-negative''

Estos son modelos de seguimiento que ajustan la fidelidad alrededor de modos de falla del mundo real (actualizaciones no atómicas, reintentos y fan-out de mensajes).

**Afirmación:** un almacén de emparejamiento debe hacer cumplir `MaxPending` e idempotencia incluso bajo intercalados (ej., "check-then-write" debe ser atómico / bloqueado; refresh no debe crear duplicados).

Lo que significa:

- Bajo solicitudes concurrentes, no puedes exceder `MaxPending` para un canal.

- Solicitudes/refreshes repetidos para el mismo `(channel, sender)` no deben crear filas pendientes duplicadas vivas.

- Ejecuciones verdes:

- ''make pairing-race'' (verificación de cap atómica/bloqueada)

- ''make pairing-idempotency''

- ''make pairing-refresh''

- ''make pairing-refresh-race''

- Rojo (esperado):

- ''make pairing-race-negative'' (carrera begin/commit de cap no atómica)

- ''make pairing-idempotency-negative''

- ''make pairing-refresh-negative''

- ''make pairing-refresh-race-negative''

**Afirmación:** la ingesta debe preservar la correlación de traza a través del fan-out y ser idempotente bajo reintentos del proveedor.

Lo que significa:

- Cuando un evento externo se convierte en múltiples mensajes internos, cada parte mantiene la misma identidad de traza/evento.

- Los reintentos no resultan en procesamiento doble.

- Si faltan los IDs de evento del proveedor, dedupe recurre a una clave segura (ej., trace ID) para evitar descartar eventos distintos.

- Verde:

- ''make ingress-trace''

- ''make ingress-trace2''

- ''make ingress-idempotency''

- ''make ingress-dedupe-fallback''

- Rojo (esperado):

- ''make ingress-trace-negative''

- ''make ingress-trace2-negative''

- ''make ingress-idempotency-negative''

- ''make ingress-dedupe-fallback-negative''

**Afirmación:** el enrutamiento debe mantener sesiones DM aisladas por defecto, y solo colapsar sesiones cuando estén explícitamente configuradas (precedencia de canal + identity links).

Lo que significa:

- Las anulaciones de dmScope específicas de canal deben ganar sobre los predeterminados globales.

- identityLinks debe colapsar solo dentro de grupos vinculados explícitos, no a través de pares no relacionados.

- Verde:

- ''make routing-precedence''

- ''make routing-identitylinks''

- Rojo (esperado):

- ''make routing-precedence-negative''

- ''make routing-identitylinks-negative''