OpenClaw Sicherheitsmodelle prüfen: Formale Verifizierung

Kennst du das? Du implementierst ein Sicherheitsfeature und denkst, du hast alle Eventualitäten abgedeckt. Doch dann schleichen sich Race Conditions oder subtile Fehlkonfigurationen ein, die dein System verwundbar machen. Formale Verifizierung hilft dir dabei, solche Logikfehler zu finden, bevor sie in Produktion Schaden anrichten.

Diese Seite zeigt dir die formalen Sicherheitsmodelle von OpenClaw (aktuell TLA+/TLC).

Hinweis: Einige ältere Links verweisen eventuell noch auf den vorherigen Projektnamen.

Das Ziel: Wir wollen maschinell geprüfte Argumente liefern, dass OpenClaw seine Sicherheitsrichtlinien (Authorization, Session-Isolierung, Tool-Gating und Schutz vor Fehlkonfigurationen) unter expliziten Annahmen erzwingt.

Was das heute ist: Eine ausführbare, Angreifer-gesteuerte Security-Regression-Suite:

• Jeder Claim besitzt einen ausführbaren Model-Check über einen endlichen Zustandsraum.
• Viele Claims sind mit einem negativen Modell gepaart, das einen Counterexample-Trace für realistische Bug-Klassen erzeugt.

Was das (noch) nicht ist: Ein Beweis, dass OpenClaw in jeder Hinsicht sicher ist oder dass die gesamte TypeScript-Implementierung fehlerfrei ist.

Wo die Modelle liegen

Die Modelle werden in einem separaten Repo gepflegt: vignesh07/openclaw-formal-models.

Wichtige Vorbehalte

• Das sind Modelle, nicht die vollständige TypeScript-Implementierung. Ein Drift zwischen Modell und Code ist möglich.
• Ergebnisse sind durch den von TLC untersuchten Zustandsraum begrenzt. „Grün“ bedeutet keine Sicherheit außerhalb der modellierten Annahmen.
• Einige Claims hängen von expliziten Umgebungsannahmen ab (z. B. korrektes Deployment).
• Die Korrektheit der Konfigurations-Inputs wird vorausgesetzt.

Ergebnisse reproduzieren

Aktuell kannst du Ergebnisse reproduzieren, indem du das Models-Repo lokal klonst und TLC ausführst (siehe unten). Zukünftige Versionen könnten Folgendes bieten:

• CI-Modelle mit öffentlichen Artefakten (Counterexample-Traces, Run-Logs).
• Ein gehosteter „Run this model“-Workflow für kleine, begrenzte Checks.

Erste Schritte:

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>

Gateway-Exponierung und Fehlkonfigurationen

Claim: Ein Binding über Loopback hinaus ohne Auth kann Remote-Compromise ermöglichen; Token/Passw