Skip to main content
De formele beveiligingsmodellen van OpenClaw (momenteel TLA+/TLC) leveren een machinaal gecontroleerd argument dat specifieke paden met het hoogste risico — autorisatie, sessie-isolatie, toolafscherming en veiligheid bij onjuiste configuratie — het beoogde beleid afdwingen, onder expliciet vermelde aannames.
Opmerking: sommige oudere links verwijzen mogelijk naar de vorige projectnaam.

​
Wat dit is

Een uitvoerbare, door aanvallers aangestuurde regressietestsuite voor beveiliging:
  • Elke claim heeft een uitvoerbare modelcontrole over een eindige toestandsruimte.
  • Veel claims hebben een gekoppeld negatief model dat een tegenvoorbeeldtrace produceert voor een realistische foutcategorie.
Dit is geen bewijs dat OpenClaw in alle opzichten veilig is en het verifieert niet de volledige TypeScript-implementatie.

​
Waar de modellen staan

De modellen worden onderhouden in een afzonderlijke repository: vignesh07/openclaw-formal-models.
Die repository is momenteel onbereikbaar (GitHub retourneert op het moment van schrijven “Repository not found”). Als deze voor jou nog steeds niet werkt, vraag dan in de OpenClaw-kanalen voor maintainers naar de huidige locatie voordat je aanneemt dat de modellen zijn verwijderd.

​
Kanttekeningen

  • Dit zijn modellen, niet de volledige TypeScript-implementatie — afwijkingen tussen model en code zijn mogelijk.
  • De resultaten worden begrensd door de toestandsruimte die TLC verkent. Groen impliceert geen beveiliging buiten de gemodelleerde aannames en grenzen.
  • Sommige claims berusten op expliciete aannames over de omgeving (bijvoorbeeld een correcte implementatie en correcte configuratie-invoer).

​
Resultaten reproduceren

Kloon de modellenrepository en voer TLC uit:
Er is nog geen CI-integratie terug naar deze repository; een toekomstige iteratie zou door CI uitgevoerde modellen met openbare artefacten (tegenvoorbeeldtraces, uitvoerlogboeken) of een gehoste workflow voor “dit model uitvoeren” kunnen toevoegen voor kleine begrensde controles.

​
Claims en doelen

​
Gateway-blootstelling en onjuiste configuratie van een open Gateway

Claim: binding buiten loopback zonder authenticatie kan compromittering op afstand mogelijk maken en vergroot de blootstelling; volgens de aannames van het model houdt een token/wachtwoord niet-geverifieerde aanvallers tegen. Zie ook docs/gateway-exposure-matrix.md in de modellenrepository.

​
Uitvoerpijplijn van Node (mogelijkheid met het hoogste risico)

Claim: exec host=node vereist (a) een toelatingslijst voor Node-opdrachten plus gedeclareerde opdrachten en (b) directe goedkeuring indien geconfigureerd; in het model worden goedkeuringen van tokens voorzien om hergebruik te voorkomen.

​
Koppelingsopslag (DM-afscherming)

Claim: koppelingsverzoeken respecteren de TTL en limieten voor openstaande verzoeken.

​
Afscherming van inkomend verkeer (vermeldingen en omzeiling via besturingsopdrachten)

Claim: in groepscontexten waarin een vermelding vereist is, kan een niet-geautoriseerde besturingsopdracht de afscherming via vermeldingen niet omzeilen.

​
Routering en isolatie van sessiesleutels

Claim: DM’s van verschillende gesprekspartners worden niet in dezelfde sessie samengevoegd, tenzij ze expliciet zijn gekoppeld of zo zijn geconfigureerd.

​
v1++-modellen: gelijktijdigheid, nieuwe pogingen en correctheid van traces

Vervolgmodellen die de getrouwheid rond storingsmodi uit de praktijk aanscherpen: niet-atomaire updates, nieuwe pogingen en berichtfan-out.

​
Gelijktijdigheid en idempotentie van de koppelingsopslag

Claim: de koppelingsopslag dwingt MaxPending en idempotentie af, zelfs bij vervlechtingen — controleren en vervolgens schrijven moet atomair/vergrendeld zijn en vernieuwen mag geen duplicaten maken. Concreet: gelijktijdige verzoeken kunnen MaxPending voor een kanaal niet overschrijden en herhaalde verzoeken/vernieuwingen voor dezelfde (channel, sender) maken geen dubbele actieve openstaande rijen.

​
Tracecorrelatie en idempotentie van inkomend verkeer

Claim: opname behoudt tracecorrelatie bij fan-out en is idempotent bij nieuwe pogingen van providers. Wanneer één externe gebeurtenis meerdere interne berichten wordt, behoudt elk onderdeel dezelfde trace-/gebeurtenisidentiteit; nieuwe pogingen worden niet dubbel verwerkt; als gebeurtenis-ID’s van de provider ontbreken, valt deduplicatie terug op een veilige sleutel (bijvoorbeeld een trace-ID) om te voorkomen dat afzonderlijke gebeurtenissen worden verwijderd. Claim: de voorrang van dmScope en identiteitskoppelingen gedragen zich deterministisch: het standaardbereik main deelt één doorlopende sessie over de DM’s van één eigenaar (de standaard voor persoonlijke agents), terwijl elk geconfigureerd isolerend bereik (per-peer, per-channel-peer, per-account-channel-peer) DM-sessies strikt gescheiden houdt. Kanaalspecifieke dmScope hebben voorrang op globale standaardwaarden; identityLinks voegen sessies alleen samen binnen expliciet gekoppelde groepen, niet tussen niet-gerelateerde gesprekspartners. Voor inboxen met meerdere gebruikers wordt verwacht dat een isolerend bereik wordt ingeschakeld (de beveiligingsaudit van de runtime beveelt dit aan wanneer deze DM-verkeer van meerdere gebruikers detecteert).

​
Gerelateerd