Verificación formal (modelos de seguridad)

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

Nota: algunos enlaces antiguos pueden referirse al nombre anterior del proyecto.

Objetivo (norte): proporcionar un argumento verificado por máquina de que OpenClaw aplica su política de seguridad prevista (autorización, aislamiento de sesión, control de herramientas y seguridad ante errores de configuración), bajo suposiciones explícitas.

Lo que es esto (hoy): una suite de regresión de seguridad ejecutable, orientada al atacante:

Cada afirmación tiene una verificación de modelo ejecutable sobre un espacio de estados finito.
Muchas afirmaciones tienen un modelo negativo asociado que produce una traza de contraejemplo para una clase de bug realista.

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

Dónde se encuentran los modelos

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

Advertencias importantes

Estos son modelos, no la implementación completa en TypeScript. Es posible que el modelo y el código diverjan.
Los resultados están acotados por el espacio de estados explorado por TLC; un resultado “verde” no implica seguridad más allá de las suposiciones y límites modelados.
Algunas afirmaciones dependen de suposiciones ambientales explícitas (por ejemplo, despliegue correcto, entradas de configuración correctas).

Reproducir resultados

Hoy, los resultados se reproducen clonando el repositorio 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 alojado de “ejecutar este modelo” para verificaciones pequeñas y acotadas

Para comenzar:

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

# Se requiere Java 11+ (TLC se ejecuta en la JVM).
# El repo incluye un `tla2tools.jar` fijado (herramientas TLA+) y proporciona `bin/tlc` + targets de Make.

make <target>

Exposición del gateway y mala configuración de gateway abierto

Afirmación: vincular más allá de loopback sin auth puede hacer posible el compromiso remoto / aumenta la exposición; token/contraseña bloquea atacantes no autorizados (según las suposiciones del modelo).

Ejecuciones verdes:
- make gateway-exposure-v2
- make gateway-exposure-v2-protected
Roja (esperada):
- make gateway-exposure-v2-negative

Consulta también: docs/gateway-exposure-matrix.md en el repositorio de modelos.

Pipeline Nodes.run (capacidad de mayor riesgo)

Afirmación: nodes.run requiere (a) allowlist de comandos del nodo más comandos declarados y (b) aprobación en vivo cuando está configurado; las aprobaciones están tokenizadas para prevenir replay (en el modelo).

Ejecuciones verdes:
- make nodes-pipeline
- make approvals-token
Rojas (esperadas):
- make nodes-pipeline-negative
- make approvals-token-negative

Almacén de vinculación (DM gating)

Afirmación: las solicitudes de vinculación respetan el TTL y los límites de solicitudes pendientes.

Ejecuciones verdes:
- make pairing
- make pairing-cap
Rojas (esperadas):
- make pairing-negative
- make pairing-cap-negative

Control de ingreso (menciones + bypass de comando de control)

Afirmación: en contextos de grupo que requieren mención, un “comando de control” no autorizado no puede evadir el gating de mención.

Verde:
- make ingress-gating
Roja (esperada):
- make ingress-gating-negative

Aislamiento de enrutamiento/clave de sesión

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

Verde:
- make routing-isolation
Roja (esperada):
- make routing-isolation-negative

v1++: modelos acotados adicionales (concurrencia, reintentos, corrección de trazas)

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

Concurrencia / idempotencia del almacén de vinculación

Afirmación: un almacén de vinculación debe aplicar MaxPending e idempotencia incluso bajo entrelazamientos (es decir, “verificar-luego-escribir” debe ser atómico / con bloqueo; el refresh no debería crear duplicados).

Lo que significa:

Bajo solicitudes concurrentes, no puedes exceder MaxPending para un canal.
Solicitudes/refreshes repetidos para el mismo (channel, sender) no deberían crear filas pendientes duplicadas.
Ejecuciones verdes:
- make pairing-race (verificación de límite atómica/con bloqueo)
- make pairing-idempotency
- make pairing-refresh
- make pairing-refresh-race
Rojas (esperadas):
- make pairing-race-negative (carrera begin/commit de límite no atómico)
- make pairing-idempotency-negative
- make pairing-refresh-negative
- make pairing-refresh-race-negative

Correlación de trazas / idempotencia de ingreso

Afirmación: la ingesta debe preservar la correlación de trazas 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 los IDs de eventos del proveedor están ausentes, el deduplicado recurre a una clave segura (por ejemplo, ID de traza) para evitar descartar eventos distintos.
Verdes:
- make ingress-trace
- make ingress-trace2
- make ingress-idempotency
- make ingress-dedupe-fallback
Rojas (esperadas):
- make ingress-trace-negative
- make ingress-trace2-negative
- make ingress-idempotency-negative
- make ingress-dedupe-fallback-negative

Precedencia de dmScope en enrutamiento + identityLinks

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

Lo que significa:

Las sobreescrituras de dmScope específicas del canal deben ganar sobre los valores globales por defecto.
Los identityLinks solo deberían colapsar dentro de grupos vinculados explícitamente, no entre pares no relacionados.
Verdes:
- make routing-precedence
- make routing-identitylinks
Rojas (esperadas):
- make routing-precedence-negative
- make routing-identitylinks-negative