> ## Documentation Index
> Fetch the complete documentation index at: https://docs2.openclaw.ai/llms.txt
> Use this file to discover all available pages before exploring further.

# 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](https://github.com/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:

```bash theme={"theme":{"light":"min-light","dark":"min-dark"}}
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](/nl/security/THREAT-MODEL-ATLAS)
* [Bijdragen aan het dreigingsmodel](/nl/security/CONTRIBUTING-THREAT-MODEL)