Verificación formal de OpenClaw: asegura tu modelo de seguri

¿Alguna vez has sentido esa duda al configurar políticas de seguridad, preguntándote si realmente cubriste todos los huecos? Validar la seguridad de forma manual es difícil y propenso a errores humanos. Por eso, en OpenClaw usamos modelos de seguridad formales para asegurar que todo funcione exactamente como esperamos.

Esta página hace un seguimiento de 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 (nuestra guía): 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 errores de configuración), bajo suposiciones explícitas.

Lo que es hoy: una suite de regresión de seguridad ejecutable y dirigida 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 bug realista.

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

Dónde viven los modelos

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

Advertencias importantes

• Estos son modelos, no la implementación completa en TypeScript. Es posible que haya desajustes entre el modelo y el código.
• 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 o entradas de configuración correctas).
• Los modelos evolucionan junto con los nuevos descubrimientos de seguridad para mantener la relevancia del sistema.

Cómo reproducir los resultados

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

• Modelos ejecutados en CI con artefactos públicos (trazas de contraejemplos, logs de ejecución).
• Un flujo de trabajo alojado de “ejecutar este modelo” para verificaciones pequeñas y acotadas.

Para empezar:

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 mala configuración de gateway abierto

Afirmación: vincular más