Formale Verifikation (Sicherheitsmodelle)

Diese Seite verfolgt OpenClaws formale Sicherheitsmodelle (heute TLA+/TLC; bei Bedarf weitere).

Hinweis: Einige ältere Links beziehen sich möglicherweise auf den vorherigen Projektnamen.

Ziel (Nordstern): Ein maschinengeprüftes Argument dafür liefern, dass OpenClaw seine beabsichtigte Sicherheitspolicy (Autorisierung, Session-Isolation, Tool-Gating und Fehlkonfigurations-Sicherheit) unter expliziten Annahmen durchsetzt.

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

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

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 Vorbehalte

• Das sind Modelle, nicht die vollständige TypeScript-Implementierung. Drift zwischen Modell und Code ist möglich.
• Ergebnisse sind durch den von TLC erkundeten Zustandsraum begrenzt; „grün” impliziert keine Sicherheit über die modellierten Annahmen und Grenzen hinaus.
• Einige Behauptungen stützen sich auf explizite Umgebungsannahmen (z.B. korrekte Deployment, korrekte Konfigurationseingaben).

Ergebnisse reproduzieren

Heute werden Ergebnisse reproduziert, indem du das Models-Repo lokal klonst und TLC ausführst (siehe unten). Eine zukünftige Iteration könnte bieten:

• CI-gesteuerte Modelle mit öffentlichen Artefakten (Gegenbeispiel-Traces, Run-Logs)
• Einen gehosteten „dieses Modell ausführen”-Workflow für kleine, begrenzte Checks

Einstieg:

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-Exposure und Open-Gateway-Fehlkonfiguration

Behauptung: Binding über Loopback hinaus ohne Auth kann Remote-Kompromittierung ermöglichen / erhöht die Angriffsfläche; Token/Passwort blockiert unauthentifizierte 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 Models-Repo.

Nodes.run Pipeline (höchstes Risiko-Capability)

Behauptung: nodes.run erfordert (a) eine Node-Command-Allowlist plus deklarierte Commands und (b) Live-Approval bei Konfiguration; Approvals 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-Requests 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 Gruppen-Kontexten die Mention 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 werden nicht in die gleiche Session zusammengelegt, es sei denn explizit verknüpft/konfiguriert.

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

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

Das sind Folgemodelle, die die Wiedergabetreue rund um reale Fehlermodi (nicht-atomare Updates, Retries und Nachrichten-Fan-out) verschärfen.

Pairing Store Nebenläufigkeit / Idempotenz

Behauptung: Ein Pairing Store muss MaxPending und Idempotenz auch unter Interleavings durchsetzen (d.h. „check-then-write” muss atomar / gesperrt sein; Refresh darf keine Duplikate erzeugen).

Was das bedeutet:

• Unter nebenläufigen Requests kann MaxPending für einen Channel nicht überschritten werden.

• Wiederholte Requests/Refreshes für das gleiche (channel, sender) dürfen keine doppelten Live-Pending-Zeilen erzeugen.

• Grüne Runs:

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

• Rot (erwartet):

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

Ingress-Trace-Korrelation / Idempotenz

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

Was das bedeutet:

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

• Retries führen nicht zu doppelter Verarbeitung.

• Wenn Provider-Event-IDs fehlen, fällt Dedupe auf einen sicheren Key (z.B. Trace-ID) zurück, 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-Priorität + identityLinks

Behauptung: Routing muss DM-Sessions standardmäßig isoliert halten und Sessions nur bei expliziter Konfiguration zusammenlegen (Channel-Priorität + Identity-Links).

Was das bedeutet:

• Channel-spezifische dmScope-Overrides müssen über globale Standardwerte gewinnen.

• identityLinks darf nur innerhalb explizit verlinkter Gruppen zusammenlegen, nicht über unverbundene Peers hinweg.

• Grün:

  • make routing-precedence
  • make routing-identitylinks

• Rot (erwartet):

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