Verificación formal (modelos de seguridad)

Los modelos formales de seguridad de OpenClaw (actualmente TLA+/TLC) proporcionan un argumento verificado por máquina de que determinadas rutas de máximo riesgo —autorización, aislamiento de sesiones, control de acceso a herramientas y seguridad ante configuraciones incorrectas— aplican la política prevista, bajo supuestos explícitos.

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

Qué es esto

Un conjunto ejecutable de pruebas de regresión de seguridad orientadas a ataques:

• Cada afirmación dispone de una comprobación de modelo ejecutable sobre un espacio de estados finito.
• Muchas afirmaciones incluyen un modelo negativo asociado que genera una traza de contraejemplo para una clase realista de errores.

Esto no demuestra que OpenClaw sea seguro en todos los aspectos ni verifica la implementación completa en TypeScript.

Dónde se encuentran los modelos

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

Consideraciones

• 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 que explora TLC. Un resultado correcto no implica seguridad más allá de los supuestos y límites modelados.
• Algunas afirmaciones dependen de supuestos explícitos sobre el entorno (por ejemplo, un despliegue correcto y entradas de configuración correctas).

Reproducción de los resultados

Clone el repositorio de modelos y ejecute TLC:

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Se requiere Java 11+ (TLC se ejecuta en la JVM).# El repositorio incluye una versión fijada de tla2tools.jar y proporciona bin/tlc, además de objetivos de Make. make <target>

Todavía no existe integración de CI con este repositorio; una iteración futura podría añadir modelos ejecutados mediante CI con artefactos públicos (trazas de contraejemplos y registros de ejecución) o un flujo de trabajo alojado de «ejecutar este modelo» para comprobaciones acotadas pequeñas.

Afirmaciones y objetivos

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

Afirmación: escuchar más allá de local loopback sin autenticación puede posibilitar un ataque remoto y aumentar la exposición; un token o una contraseña bloquean a los atacantes no autenticados, según los supuestos del modelo.

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

Canalización de ejecución de Node (capacidad de máximo riesgo)

Afirmación: exec host=node requiere (a) una lista de comandos permitidos de Node junto con comandos declarados y (b) aprobación en tiempo real cuando esté configurada; en el modelo, las aprobaciones utilizan tokens para evitar la reutilización.

Almacén de vinculación (control de acceso a mensajes directos)

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

Control de acceso de entrada (menciones y omisión mediante comandos de control)

Afirmación: en contextos de grupo que requieren una mención, un comando de control no autorizado no puede eludir el control de acceso mediante menciones.

Enrutamiento y aislamiento de claves de sesión

Afirmación: los mensajes directos de distintos interlocutores no se agrupan en la misma sesión, salvo que se vinculen o configuren explícitamente.

Modelos v1++: concurrencia, reintentos y corrección de trazas

Modelos posteriores que mejoran la fidelidad respecto a modos de fallo reales: actualizaciones no atómicas, reintentos y distribución de mensajes.

Concurrencia e idempotencia del almacén de vinculación

Afirmación: el almacén de vinculación aplica MaxPending y la idempotencia incluso con intercalaciones: la comprobación seguida de escritura debe ser atómica o estar bloqueada, y la actualización no debe crear duplicados. En concreto, las solicitudes simultáneas no pueden superar MaxPending para un canal, y las solicitudes o actualizaciones repetidas para el mismo (channel, sender) no crean filas pendientes activas duplicadas.

Correlación e idempotencia de trazas de entrada

Afirmación: la ingesta conserva la correlación de trazas durante la distribución y es idempotente ante los reintentos del proveedor. Cuando un evento externo se convierte en varios mensajes internos, cada parte mantiene la misma identidad de traza o evento; los reintentos no provocan un procesamiento duplicado; si faltan los identificadores de evento del proveedor, la deduplicación recurre a una clave segura (por ejemplo, el identificador de traza) para evitar descartar eventos distintos.

Precedencia de dmScope e identityLinks en el enrutamiento

Afirmación: el enrutamiento mantiene aisladas de forma predeterminada las sesiones de mensajes directos y solo las agrupa cuando se configura explícitamente mediante la precedencia de canales y los vínculos de identidad. Las sustituciones de dmScope específicas de cada canal tienen prioridad sobre los valores predeterminados globales; identityLinks agrupa sesiones únicamente dentro de grupos vinculados explícitamente, no entre interlocutores sin relación.

Contenido relacionado

• Modelo de amenazas
• Contribuir al modelo de amenazas
• Respuesta ante incidentes