Verificación formal (modelos de seguridad)

Esta página hace seguimiento de 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 (guía principal): proporcionar un argumento verificado por máquina de que OpenClaw aplica su política de seguridad prevista (autorización, aislamiento de sesiones, control de herramientas y seguridad ante configuraciones incorrectas), bajo supuestos explícitos.

Qué es esto (hoy): un conjunto de regresión de seguridad ejecutable e impulsado por atacantes:

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

Qué no es esto (todavía): una prueba de que "OpenClaw es seguro en todos los aspectos" o de que la implementación completa en TypeScript es correcta.

# Dónde viven los modelos

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

# Advertencias importantes

• Estos son modelos, no la implementación completa en TypeScript. Es posible que haya divergencias entre el modelo y el 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 (por ejemplo, despliegue correcto, entradas de configuración correctas).

# Reproducir los resultados

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

• modelos ejecutados en CI con artefactos públicos (trazas de contraejemplo, registros de ejecución)
• un flujo de trabajo alojado de "ejecutar este modelo" para comprobaciones pequeñas y acotadas

Primeros pasos:

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

# Java 11+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>

# Exposición del Gateway y configuración incorrecta de Gateway abierto

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

• Ejecuciones verdes:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Rojas (esperadas):
  • make gateway-exposure-v2-negative

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

# Canalización de exec de Node (capacidad de mayor riesgo)

Afirmación: exec host=node requiere (a) una lista de comandos Node permitidos más comandos declarados y (b) aprobación en vivo cuando está configurado; las aprobaciones se tokenizan para evitar la reproducción (en el modelo).

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

# Almacén de emparejamiento (control de DM)

Afirmación: las solicitudes de emparejamiento 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 entrada (menciones + omisión por comando de control)

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

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

# Aislamiento de enrutamiento/clave de sesión

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

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

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

Estos son modelos posteriores que refuerzan la fidelidad en torno a modos de fallo del mundo real (actualizaciones no atómicas, reintentos y distribución de mensajes).

# Concurrencia / idempotencia del almacén de emparejamiento

Afirmación: un almacén de emparejamiento debería aplicar MaxPending y la idempotencia incluso bajo intercalados (es decir, "comprobar y luego escribir" debe ser atómico / bloqueado; la actualización no debería crear duplicados).

Qué significa:

• Bajo solicitudes concurrentes, no puedes superar MaxPending para un canal.

• Las solicitudes/actualizaciones repetidas para el mismo (channel, sender) no deberían crear filas pendientes vivas duplicadas.

• Ejecuciones verdes:

  • make pairing-race (comprobación de límite atómica/bloqueada)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Rojas (esperadas):

  • make pairing-race-negative (carrera de límite no atómica begin/commit)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

# Correlación de trazas de entrada / idempotencia

Afirmación: la ingesta debería preservar la correlación de trazas durante la distribución y ser idempotente bajo reintentos del proveedor.

Qué significa:

• Cuando un evento externo se convierte en varios mensajes internos, cada parte mantiene la misma identidad de traza/evento.

• Los reintentos no provocan procesamiento doble.

• Si faltan los IDs de eventos del proveedor, la deduplicación recurre a una clave segura (por ejemplo, ID de traza) para evitar descartar eventos distintos.

• Verde:

  • 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 de enrutamiento + identityLinks

Afirmación: el enrutamiento debe mantener aisladas las sesiones de DM de forma predeterminada, y solo colapsar sesiones cuando se configura explícitamente (precedencia de canal + enlaces de identidad).

Qué significa:

• Las anulaciones de dmScope específicas del canal deben prevalecer sobre los valores predeterminados globales.

• identityLinks debería colapsar solo dentro de grupos vinculados explícitos, no entre pares no relacionados.

• Verde:

  • make routing-precedence
  • make routing-identitylinks

• Rojas (esperadas):

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

# Relacionado

• Modelo de amenazas
• Contribuir al modelo de amenazas