Formal Verification (Sicherheitsmodelle)

Diese Seite dokumentiert OpenClaws formale Sicherheitsmodelle (aktuell TLA+/TLC; weitere nach Bedarf).

Hinweis: Einige ältere Links verweisen möglicherweise noch auf den früheren Projektnamen.

Ziel (langfristig): Ein maschinengeprüfter Nachweis, dass OpenClaw seine beabsichtigte Sicherheitsrichtlinie durchsetzt (Autorisierung, Session-Isolation, Tool-Gating und Schutz vor Fehlkonfiguration) – unter expliziten Annahmen.

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

• Jede Behauptung hat einen ausführbaren Model-Check über einen endlichen Zustandsraum.
• Viele Behauptungen haben ein zugehöriges Negativ-Modell, das einen Counterexample-Trace für eine realistische Bug-Klasse erzeugt.

Was das (noch) nicht ist: Ein Beweis, dass “OpenClaw in jeder Hinsicht sicher ist” oder dass die vollständige TypeScript-Implementierung korrekt ist.

Wo die Modelle liegen

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

Wichtige Einschränkungen

• Das sind Modelle, nicht die vollständige TypeScript-Implementierung. Abweichungen zwischen Modell und Code sind möglich.
• Die Ergebnisse sind durch den von TLC erkundeten Zustandsraum begrenzt; “grün” bedeutet nicht, dass Sicherheit über die modellierten Annahmen und Grenzen hinaus garantiert ist.
• Einige Behauptungen basieren auf expliziten Umgebungsannahmen (z. B. korrekte Bereitstellung, korrekte Konfigurationseingaben).

Ergebnisse reproduzieren

Aktuell werden Ergebnisse reproduziert, indem du das Modell-Repo lokal clonst und TLC ausführst (siehe unten). Eine zukünftige Version könnte bieten:

• CI-gesteuerte Modelle mit öffentlichen Artefakten (Counterexample-Traces, Run-Logs)
• einen gehosteten “run this model”-Workflow für kleine, begrenzte Checks

Los geht’s:

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Java 11+ erforderlich (TLC läuft auf der JVM).
# Das Repo enthält eine gepinnte `tla2tools.jar` (TLA+ Tools) und stellt `bin/tlc` + Make-Targets bereit.

make <target>

Gateway-Exposition und offene Gateway-Fehlkonfiguration

Behauptung: Binding über Loopback hinaus ohne Auth kann Remote-Kompromittierung ermöglichen / erhöht die Exposition; Token/Passwort blockiert unautorisierte Angreifer (gemäß den Modellannahmen).

• Grüne Runs:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Rot (erwartet):
  • make gateway-exposure-v2-negative

Siehe auch: docs/gateway-exposure-matrix.md im Modell-Repo.

Nodes.run-Pipeline (höchstes Risiko)

Behauptung: nodes.run erfordert (a) eine Node-Command-Allowlist plus deklarierte Befehle und (b) Live-Freigabe, wenn konfiguriert; Freigaben sind tokenisiert, um Replay zu verhindern (im Modell).

• Grüne Runs:
  • make nodes-pipeline
  • make approvals-token
• Rot (erwartet):
  • make nodes-pipeline-negative
  • make approvals-token-negative

Pairing-Store (DM-Gating)

Behauptung: Pairing-Anfragen respektieren TTL und Pending-Request-Caps.

• Grüne Runs:
  • make pairing
  • make pairing-cap
• Rot (erwartet):
  • make pairing-negative
  • make pairing-cap-negative

Ingress-Gating (Mentions + Control-Command-Bypass)

Behauptung: In Gruppenkontexten, die eine Erwähnung erfordern, kann ein unautorisierter “Control Command” das Mention-Gating nicht umgehen.

• Grün:
  • make ingress-gating
• Rot (erwartet):
  • make ingress-gating-negative

Routing/Session-Key-Isolation

Behauptung: DMs von unterschiedlichen Peers kollabieren nicht in dieselbe Session, es sei denn, sie sind explizit verlinkt/konfiguriert.

• Grün:
  • make routing-isolation
• Rot (erwartet):
  • make routing-isolation-negative

v1++: Zusätzliche begrenzte Modelle (Concurrency, Retries, Trace-Korrektheit)

Das sind Folgemodelle, die die Genauigkeit rund um reale Fehlermodi erhöhen (nicht-atomare Updates, Retries und Message-Fan-out).

Pairing-Store Concurrency / Idempotenz

Behauptung: Ein Pairing-Store sollte MaxPending und Idempotenz auch bei Interleavings durchsetzen (d. h. “check-then-write” muss atomar/gelockt sein; Refresh sollte keine Duplikate erzeugen).

Was das bedeutet:

• Bei gleichzeitigen Anfragen kannst du MaxPending für einen Channel nicht überschreiten.

• Wiederholte Anfragen/Refreshes für dasselbe (channel, sender) sollten keine doppelten Live-Pending-Zeilen erzeugen.

• Grüne Runs:

  • make pairing-race (atomarer/gelockter Cap-Check)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Rot (erwartet):

  • make pairing-race-negative (nicht-atomares begin/commit Cap-Race)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

Ingress-Trace-Korrelation / Idempotenz

Behauptung: Ingestion sollte Trace-Korrelation über Fan-out hinweg bewahren und idempotent bei Provider-Retries sein.

Was das bedeutet:

• Wenn ein externes Event zu mehreren internen Nachrichten wird, behält jeder Teil dieselbe Trace/Event-Identität.

• Retries führen nicht zu doppelter Verarbeitung.

• Wenn Provider-Event-IDs fehlen, fällt Dedupe auf einen sicheren Key zurück (z. B. Trace-ID), um das Verwerfen unterschiedlicher Events zu vermeiden.

• Grün:

  • make ingress-trace
  • make ingress-trace2
  • make ingress-idempotency
  • make ingress-dedupe-fallback

• Rot (erwartet):

  • make ingress-trace-negative
  • make ingress-trace2-negative
  • make ingress-idempotency-negative
  • make ingress-dedupe-fallback-negative

Routing dmScope-Präzedenz + identityLinks

Behauptung: Routing muss DM-Sessions standardmäßig isoliert halten und Sessions nur bei expliziter Konfiguration kollabieren lassen (Channel-Präzedenz + Identity-Links).

Was das bedeutet:

• Channel-spezifische dmScope-Overrides müssen Vorrang vor globalen Defaults haben.

• identityLinks sollten nur innerhalb explizit verlinkter Gruppen kollabieren, nicht über unverbundene Peers hinweg.

• Grün:

  • make routing-precedence
  • make routing-identitylinks

• Rot (erwartet):

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