Formele verificatie (beveiligingsmodellen)

Deze pagina volgt OpenClaw's formele beveiligingsmodellen (TLA+/TLC vandaag; meer indien nodig).

Opmerking: sommige oudere links kunnen verwijzen naar de vorige projectnaam.

Doel (leidster): een machinaal gecontroleerd argument leveren dat OpenClaw zijn bedoelde beveiligingsbeleid afdwingt (autorisatie, sessie-isolatie, toolafscherming en veiligheid bij misconfiguratie), onder expliciete aannames.

Wat dit is (vandaag): een uitvoerbare, door aanvallers gedreven regressiesuite voor beveiliging:

• Elke claim heeft een uitvoerbare modelcontrole over een eindige toestandsruimte.
• Veel claims hebben een gekoppeld negatief model dat een tegenvoorbeeldtrace oplevert voor een realistische bugklasse.

Wat dit niet is (nog): een bewijs dat "OpenClaw in alle opzichten veilig is" of dat de volledige TypeScript-implementatie correct is.

# Waar de modellen staan

Modellen worden onderhouden in een aparte repo: vignesh07/openclaw-formal-models.

# Belangrijke kanttekeningen

• Dit zijn modellen, niet de volledige TypeScript-implementatie. Afwijkingen tussen model en code zijn mogelijk.
• Resultaten worden begrensd door de toestandsruimte die door TLC is verkend; "groen" impliceert geen beveiliging buiten de gemodelleerde aannames en grenzen.
• Sommige claims steunen op expliciete omgevingsaannames (bijv. correcte deployment, correcte configuratie-invoer).

# Resultaten reproduceren

Vandaag worden resultaten gereproduceerd door de modellenrepo lokaal te klonen en TLC uit te voeren (zie hieronder). Een toekomstige iteratie zou kunnen bieden:

• Door CI uitgevoerde modellen met openbare artefacten (tegenvoorbeeldtraces, runlogs)
• een gehoste workflow "voer dit model uit" voor kleine, begrensde controles

Aan de slag:

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-blootstelling en open Gateway-misconfiguratie

Claim: binden buiten loopback zonder auth kan externe compromittering mogelijk maken / vergroot de blootstelling; token/wachtwoord blokkeert niet-geauthenticeerde aanvallers (volgens de modelaannames).

• Groene runs:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Rood (verwacht):
  • make gateway-exposure-v2-negative

Zie ook: docs/gateway-exposure-matrix.md in de modellenrepo.

# Node-exec-pijplijn (capaciteit met het hoogste risico)

Claim: exec host=node vereist (a) een allowlist voor node-opdrachten plus gedeclareerde opdrachten en (b) live goedkeuring wanneer geconfigureerd; goedkeuringen zijn getokeniseerd om replay te voorkomen (in het model).

• Groene runs:
  • make nodes-pipeline
  • make approvals-token
• Rood (verwacht):
  • make nodes-pipeline-negative
  • make approvals-token-negative

# Koppelingsopslag (DM-afscherming)

Claim: koppelingsverzoeken respecteren TTL en limieten voor openstaande verzoeken.

• Groene runs:
  • make pairing
  • make pairing-cap
• Rood (verwacht):
  • make pairing-negative
  • make pairing-cap-negative

# Ingress-afscherming (vermeldingen + omzeiling via besturingsopdracht)

Claim: in groepscontexten die een vermelding vereisen, kan een ongeautoriseerde "besturingsopdracht" de vermeldingsafscherming niet omzeilen.

• Groen:
  • make ingress-gating
• Rood (verwacht):
  • make ingress-gating-negative

# Routerings-/sessiesleutelisolatie

Claim: DM's van verschillende peers worden niet samengevoegd tot dezelfde sessie, tenzij ze expliciet gekoppeld/geconfigureerd zijn.

• Groen:
  • make routing-isolation
• Rood (verwacht):
  • make routing-isolation-negative

# v1++: aanvullende begrensde modellen (concurrency, retries, tracecorrectheid)

Dit zijn vervolgmodellen die de getrouwheid aanscherpen rond realistische foutmodi (niet-atomaire updates, retries en message-fan-out).

# Concurrency / idempotentie van koppelingsopslag

Claim: een koppelingsopslag moet MaxPending en idempotentie afdwingen, zelfs bij interleavings (d.w.z. "controleer-dan-schrijf" moet atomair / vergrendeld zijn; vernieuwen mag geen duplicaten maken).

Wat dit betekent:

• Bij gelijktijdige verzoeken kun je MaxPending voor een kanaal niet overschrijden.

• Herhaalde verzoeken/vernieuwingen voor dezelfde (channel, sender) mogen geen dubbele live openstaande rijen maken.

• Groene runs:

  • make pairing-race (atomaire/vergrendelde limietcontrole)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Rood (verwacht):

  • make pairing-race-negative (niet-atomaire begin/commit-limietrace)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

# Ingress-tracecorrelatie / idempotentie

Claim: ingestion moet tracecorrelatie over fan-out heen behouden en idempotent zijn bij provider-retries.

Wat dit betekent:

• Wanneer één externe gebeurtenis meerdere interne berichten wordt, behoudt elk deel dezelfde trace-/gebeurtenisidentiteit.

• Retries leiden niet tot dubbele verwerking.

• Als provider-event-ID's ontbreken, valt deduplicatie terug op een veilige sleutel (bijv. trace-ID) om te voorkomen dat verschillende gebeurtenissen worden weggegooid.

• Groen:

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

• Rood (verwacht):

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

# Voorrang van routing dmScope + identityLinks

Claim: routing moet DM-sessies standaard geïsoleerd houden en sessies alleen samenvoegen wanneer dit expliciet is geconfigureerd (kanaalvoorrang + identity links).

Wat dit betekent:

• Kanaalspecifieke dmScope-overrides moeten winnen van globale defaults.

• identityLinks mogen alleen samenvoegen binnen expliciet gekoppelde groepen, niet tussen niet-gerelateerde peers.

• Groen:

  • make routing-precedence
  • make routing-identitylinks

• Rood (verwacht):

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

# Gerelateerd

• Dreigingsmodel
• Bijdragen aan het dreigingsmodel