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).

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

Objetivo (estrella polar): proporcionar un argumento verificado por máquina de que OpenClaw hace cumplir su política de seguridad prevista (autorización, aislamiento de sesión, bloqueo de herramientas y seguridad frente a configuraciones erróneas), bajo suposiciones explícitas.

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

• 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 un rastro de contraejemplo para una clase de error realista.

Lo que esto no es (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 residen 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 exista una divergencia 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 las suposiciones y límites modelados.
• Algunas afirmaciones se basan en suposiciones ambientales explícitas (por ejemplo, implementación correcta, entradas de configuración correctas).

Reproducción de resultados

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

• Modelos ejecutados por CI con artefactos públicos (rastros de contraejemplo, registros de ejecución)
• un flujo de trabajo alojado “ejecutar este modelo” para verificaciones pequeñas y acotadas

Para comenzar:

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 de la puerta de enlace y configuración errónea de la puerta de enlace abierta

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

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

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

Canal de ejecución de nodos (capacidad de mayor riesgo)

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

• Ejecuciones verdes:
  • make nodes-pipeline
  • make approvals-token
• Rojo (esperado):
  • make nodes-pipeline-negative
  • make approvals-token-negative

Almacén de emparejamiento (bloqueo 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
• Rojo (esperado):
  • make pairing-negative
  • make pairing-cap-negative

Bloqueo de entrada (menciones + omisión de comando de control)

Afirmación: en contextos grupales que requieren mención, un “comando de control” no autorizado no puede evitar el filtrado por mención.

• Verde:
  • make ingress-gating
• Rojo (esperado):
  • make ingress-gating-negative

Aislamiento de enrutamiento/clave de sesión

Afirmación: los MD de distintos pares no se 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

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

Estos son modelos de seguimiento que ajustan la fidelidad en torno a los modos de falla 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 debe hacer cumplir MaxPending y la idempotencia incluso bajo intercalaciones (es decir, “verificar-then-escribir” debe ser atómico/bloqueado; la actualización no debe crear duplicados).

Lo que significa:

• En solicitudes concurrentes, no puedes exceder MaxPending para un canal.

• Las solicitudes/actualizaciones repetidas para el mismo (channel, sender) no deben crear filas pendientes en vivo duplicadas.

• Ejecuciones verdes:

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

• Rojo (esperado):

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

Correlación de trazas de entrada / idempotencia

Afirmación: la ingesta debe preservar la correlación de trazas a través de la distribución (fan-out) y ser idempotente bajo los reintentos del proveedor.

Lo que significa:

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

• Los reintentos no dan lugar a un procesamiento doble.

• Si faltan los IDs de eventos del proveedor, la deduplicación recurre a una clave segura (p. ej., ID de traza) 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

Precedencia de dmScope de enrutamiento + identityLinks

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

Lo que significa:

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

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

• Verde:

  • make routing-precedence
  • make routing-identitylinks

• Rojo (esperado):

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

Relacionado

• Modelo de amenazas
• Contribución al modelo de amenazas