Security

Formale Verifikation (Sicherheitsmodelle)

Die formalen Sicherheitsmodelle von OpenClaw (derzeit TLA+/TLC) liefern ein maschinell geprüftes Argument dafür, dass bestimmte Pfade mit dem höchsten Risiko — Autorisierung, Sitzungsisolation, Tool-Zugriffskontrolle und Sicherheit bei Fehlkonfigurationen — unter ausdrücklich genannten Annahmen die vorgesehenen Richtlinien durchsetzen.

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

Was dies ist

Eine ausführbare, angriffsorientierte Suite für Sicherheitsregressionstests:

Für jede Aussage gibt es eine ausführbare Modellprüfung über einen endlichen Zustandsraum.
Für viele Aussagen gibt es ein zugehöriges Negativmodell, das für eine realistische Fehlerklasse eine Gegenbeispielspur erzeugt.

Dies ist kein Beweis dafür, dass OpenClaw in jeder Hinsicht sicher ist, und es überprüft nicht die vollständige TypeScript-Implementierung.

Speicherort der Modelle

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

Einschränkungen

Es handelt sich um Modelle, nicht um die vollständige TypeScript-Implementierung — Abweichungen zwischen Modell und Code sind möglich.
Die Ergebnisse sind durch den von TLC untersuchten Zustandsraum begrenzt. Ein grünes Ergebnis bedeutet keine Sicherheit über die modellierten Annahmen und Grenzen hinaus.
Einige Aussagen beruhen auf ausdrücklichen Annahmen zur Umgebung (beispielsweise eine korrekte Bereitstellung und korrekte Konfigurationseingaben).

Ergebnisse reproduzieren

Klonen Sie das Modell-Repository und führen Sie TLC aus:

bash

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Java 11+ erforderlich (TLC wird auf der JVM ausgeführt).# Das Repository enthält eine festgelegte Version von tla2tools.jar und stellt bin/tlc sowie Make-Ziele bereit. make <target>

Eine CI-Integration zurück in dieses Repository gibt es noch nicht. Eine zukünftige Version könnte über CI ausgeführte Modelle mit öffentlichen Artefakten (Gegenbeispielspuren, Ausführungsprotokolle) oder einen gehosteten „Dieses Modell ausführen“-Workflow für kleine, begrenzte Prüfungen ergänzen.

Aussagen und Ziele

Gateway-Exposition und Fehlkonfiguration eines offenen Gateways

Aussage: Eine Bindung außerhalb der Loopback-Schnittstelle ohne Authentifizierung kann eine Kompromittierung aus der Ferne ermöglichen und erhöht die Exposition. Ein Token oder Passwort blockiert gemäß den Annahmen des Modells nicht authentifizierte Angreifer.

Ergebnis	Ziele
Grün	`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-Repository.

Node-Ausführungspipeline (Funktion mit dem höchsten Risiko)

Aussage: exec host=node erfordert (a) eine Positivliste für Node-Befehle sowie deklarierte Befehle und (b) eine aktuelle Genehmigung, sofern diese konfiguriert ist. Im Modell werden Genehmigungen mit Token versehen, um eine erneute Verwendung zu verhindern.

Ergebnis	Ziele
Grün	`make nodes-pipeline`, `make approvals-token`
Rot (erwartet)	`make nodes-pipeline-negative`, `make approvals-token-negative`

Kopplungsspeicher (DM-Zugriffskontrolle)

Aussage: Kopplungsanfragen berücksichtigen die TTL und Obergrenzen für ausstehende Anfragen.

Ergebnis	Ziele
Grün	`make pairing`, `make pairing-cap`
Rot (erwartet)	`make pairing-negative`, `make pairing-cap-negative`

Eingangs-Zugriffskontrolle (Erwähnungen und Umgehung durch Steuerbefehle)

Aussage: In Gruppenkontexten, die eine Erwähnung erfordern, kann ein nicht autorisierter Steuerbefehl die Zugriffskontrolle für Erwähnungen nicht umgehen.

Ergebnis	Ziele
Grün	`make ingress-gating`
Rot (erwartet)	`make ingress-gating-negative`

Routing und Isolation von Sitzungsschlüsseln

Aussage: DMs von unterschiedlichen Kommunikationspartnern werden nicht in derselben Sitzung zusammengeführt, sofern sie nicht ausdrücklich verknüpft oder entsprechend konfiguriert sind.

Ergebnis	Ziele
Grün	`make routing-isolation`
Rot (erwartet)	`make routing-isolation-negative`

v1++-Modelle: Nebenläufigkeit, Wiederholungsversuche und Korrektheit von Spuren

Weiterführende Modelle, die die Übereinstimmung mit realen Fehlermodi verbessern: nicht atomare Aktualisierungen, Wiederholungsversuche und Nachrichten-Fan-out.

Nebenläufigkeit und Idempotenz des Kopplungsspeichers

Aussage: Der Kopplungsspeicher erzwingt MaxPending und Idempotenz auch bei verzahnten Abläufen — Prüfung und anschließendes Schreiben müssen atomar beziehungsweise gesperrt erfolgen, und eine Aktualisierung darf keine Duplikate erzeugen. Konkret gilt: Gleichzeitige Anfragen dürfen MaxPending für einen Kanal nicht überschreiten, und wiederholte Anfragen oder Aktualisierungen für dasselbe (channel, sender) erzeugen keine doppelten aktiven ausstehenden Zeilen.

Ergebnis	Ziele
Grün	`make pairing-race` (atomare/gesperrte Prüfung der Obergrenze), `make pairing-idempotency`, `make pairing-refresh`, `make pairing-refresh-race`
Rot (erwartet)	`make pairing-race-negative` (nicht atomare Begin-/Commit-Konkurrenzsituation bei der Obergrenze), `make pairing-idempotency-negative`, `make pairing-refresh-negative`, `make pairing-refresh-race-negative`

Korrelation und Idempotenz von Eingangsspuren

Aussage: Die Aufnahme erhält die Spurenkorrelation über Fan-out hinweg und ist bei Wiederholungsversuchen des Providers idempotent. Wenn ein externes Ereignis in mehrere interne Nachrichten aufgeteilt wird, behält jeder Teil dieselbe Spuren-/Ereignisidentität. Wiederholungsversuche führen nicht zu einer doppelten Verarbeitung. Wenn Ereignis-IDs des Providers fehlen, greift die Deduplizierung auf einen sicheren Schlüssel zurück (beispielsweise die Spuren-ID), damit unterschiedliche Ereignisse nicht verworfen werden.

Ergebnis	Ziele
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-Priorität von dmScope und identityLinks

Aussage: Das Routing hält DM-Sitzungen standardmäßig isoliert und führt Sitzungen nur dann zusammen, wenn dies über die Kanalpriorität und Identitätsverknüpfungen ausdrücklich konfiguriert ist. Kanalspezifische Überschreibungen von dmScope haben Vorrang vor globalen Standardwerten. identityLinks führen Sitzungen nur innerhalb ausdrücklich verknüpfter Gruppen zusammen, nicht über voneinander unabhängige Kommunikationspartner hinweg.

Ergebnis	Ziele
Grün	`make routing-precedence`, `make routing-identitylinks`
Rot (erwartet)	`make routing-precedence-negative`, `make routing-identitylinks-negative`