Verificación formal (modelos de seguridad)

Los modelos formales de seguridad de OpenClaw (TLA+/TLC actualmente) 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 atacantes:

• Cada afirmación cuenta con una comprobación de modelo ejecutable sobre un espacio de estados finito.
• Muchas afirmaciones cuentan con 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 existan divergencias entre el modelo y el código.
• Los resultados están limitados por el espacio de estados que explora TLC. Un resultado satisfactorio 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 una integración de CI con este repositorio; una futura iteración 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: vincular más allá de la interfaz de bucle local sin autenticación puede posibilitar una vulneración remota y aumentar la exposición; según los supuestos del modelo, un token o una contraseña bloquean a los atacantes no autenticados.

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

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

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

Almacén de emparejamiento (control de acceso a mensajes directos)

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

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

Afirmación: en contextos de grupo que requieran 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 interlocutores distintos no se agrupan en la misma sesión, salvo que estén vinculados o configurados explícitamente.

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

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

Concurrencia e idempotencia del almacén de emparejamiento

Afirmación: el almacén de emparejamiento aplica MaxPending y la idempotencia incluso cuando las operaciones se intercalan: 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 conserva 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 utiliza como alternativa una clave segura (por ejemplo, el identificador de traza) para evitar descartar eventos distintos.

Precedencia de dmScope en el enrutamiento e identityLinks

Afirmación: la precedencia de dmScope y los vínculos de identidad se comportan de forma determinista: el ámbito predeterminado main comparte una única sesión continua entre los mensajes directos de un solo propietario (la configuración predeterminada del agente personal), mientras que cualquier ámbito de aislamiento configurado (per-peer, per-channel-peer, per-account-channel-peer) mantiene las sesiones de mensajes directos estrictamente separadas. Las anulaciones de dmScope específicas del canal prevalecen sobre los valores predeterminados globales; identityLinks agrupa sesiones únicamente dentro de grupos vinculados explícitamente, no entre interlocutores no relacionados. Se espera que las bandejas de entrada multiusuario adopten un ámbito de aislamiento (la auditoría de seguridad del entorno de ejecución lo recomienda cuando detecta tráfico de mensajes directos de varios usuarios).

Contenido relacionado

• Modelo de amenazas
• Contribución al modelo de amenazas
• Respuesta ante incidentes