> ## 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.

# Weryfikacja formalna (modele bezpieczeństwa)

Ta strona śledzi **formalne modele bezpieczeństwa** OpenClaw (obecnie TLA+/TLC; kolejne w razie potrzeby).

> Uwaga: niektóre starsze linki mogą odnosić się do poprzedniej nazwy projektu.

**Cel (gwiazda północna):** dostarczyć sprawdzony maszynowo argument, że OpenClaw egzekwuje swoją
zamierzoną politykę bezpieczeństwa (autoryzacja, izolacja sesji, bramkowanie narzędzi i
bezpieczeństwo przy błędnej konfiguracji), przy jawnych założeniach.

**Czym to jest (obecnie):** wykonywalny, sterowany przez atakującego **zestaw regresyjny bezpieczeństwa**:

* Każde twierdzenie ma uruchamialne sprawdzenie modelu w skończonej przestrzeni stanów.
* Wiele twierdzeń ma sparowany **model negatywny**, który generuje ślad kontrprzykładu dla realistycznej klasy błędów.

**Czym to nie jest (jeszcze):** dowód, że „OpenClaw jest bezpieczny pod każdym względem” albo że pełna implementacja TypeScript jest poprawna.

## Gdzie znajdują się modele

Modele są utrzymywane w osobnym repozytorium: [vignesh07/openclaw-formal-models](https://github.com/vignesh07/openclaw-formal-models).

## Ważne zastrzeżenia

* To są **modele**, a nie pełna implementacja TypeScript. Możliwy jest rozdźwięk między modelem a kodem.
* Wyniki są ograniczone przestrzenią stanów eksplorowaną przez TLC; „zielony” wynik nie oznacza bezpieczeństwa poza modelowanymi założeniami i ograniczeniami.
* Niektóre twierdzenia opierają się na jawnych założeniach środowiskowych (np. poprawne wdrożenie, poprawne dane wejściowe konfiguracji).

## Odtwarzanie wyników

Obecnie wyniki odtwarza się przez lokalne sklonowanie repozytorium modeli i uruchomienie TLC (zobacz poniżej). Przyszła iteracja mogłaby oferować:

* modele uruchamiane w CI z publicznymi artefaktami (ślady kontrprzykładów, logi uruchomień)
* hostowany przepływ „uruchom ten model” dla małych, ograniczonych sprawdzeń

Pierwsze kroki:

```bash theme={"theme":{"light":"min-light","dark":"min-dark"}}
git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Wymagane Java 11+ (TLC działa na JVM).
# Repozytorium zawiera dostarczony, przypięty `tla2tools.jar` (narzędzia TLA+) oraz udostępnia `bin/tlc` + cele Make.

make <target>
```

### Ekspozycja Gateway i błędna konfiguracja otwartego Gateway

**Twierdzenie:** wiązanie poza loopback bez uwierzytelniania może umożliwić zdalne przejęcie / zwiększa ekspozycję; token/hasło blokuje nieuwierzytelnionych atakujących (zgodnie z założeniami modelu).

* Zielone uruchomienia:
  * `make gateway-exposure-v2`
  * `make gateway-exposure-v2-protected`
* Czerwone (oczekiwane):
  * `make gateway-exposure-v2-negative`

Zobacz też: `docs/gateway-exposure-matrix.md` w repozytorium modeli.

### Potok exec Node (funkcja najwyższego ryzyka)

**Twierdzenie:** `exec host=node` wymaga (a) listy dozwolonych poleceń Node oraz zadeklarowanych poleceń i (b) zatwierdzenia na żywo, gdy jest skonfigurowane; zatwierdzenia są tokenizowane, aby zapobiec powtórnemu użyciu (w modelu).

* Zielone uruchomienia:
  * `make nodes-pipeline`
  * `make approvals-token`
* Czerwone (oczekiwane):
  * `make nodes-pipeline-negative`
  * `make approvals-token-negative`

### Magazyn parowania (bramkowanie DM)

**Twierdzenie:** żądania parowania respektują TTL i limity oczekujących żądań.

* Zielone uruchomienia:
  * `make pairing`
  * `make pairing-cap`
* Czerwone (oczekiwane):
  * `make pairing-negative`
  * `make pairing-cap-negative`

### Bramkowanie wejścia (wzmianki + obejście polecenia kontrolnego)

**Twierdzenie:** w kontekstach grupowych wymagających wzmianki nieautoryzowane „polecenie kontrolne” nie może ominąć bramkowania wzmianek.

* Zielone:
  * `make ingress-gating`
* Czerwone (oczekiwane):
  * `make ingress-gating-negative`

### Izolacja routingu/klucza sesji

**Twierdzenie:** DM od różnych nadawców nie są łączone w tę samą sesję, chyba że są jawnie powiązane/skonfigurowane.

* Zielone:
  * `make routing-isolation`
* Czerwone (oczekiwane):
  * `make routing-isolation-negative`

## v1++: dodatkowe modele ograniczone (współbieżność, ponowienia, poprawność śladu)

To są modele uzupełniające, które zwiększają wierność wobec rzeczywistych trybów awarii (nieatomowe aktualizacje, ponowienia i rozsyłanie wiadomości).

### Współbieżność / idempotencja magazynu parowania

**Twierdzenie:** magazyn parowania powinien egzekwować `MaxPending` i idempotencję nawet przy przeplotach (tj. „sprawdź, potem zapisz” musi być atomowe / zablokowane; odświeżenie nie powinno tworzyć duplikatów).

Co to oznacza:

* Przy współbieżnych żądaniach nie można przekroczyć `MaxPending` dla kanału.

* Powtarzane żądania/odświeżenia dla tego samego `(channel, sender)` nie powinny tworzyć zduplikowanych aktywnych wierszy oczekujących.

* Zielone uruchomienia:
  * `make pairing-race` (atomowe/zablokowane sprawdzenie limitu)
  * `make pairing-idempotency`
  * `make pairing-refresh`
  * `make pairing-refresh-race`

* Czerwone (oczekiwane):
  * `make pairing-race-negative` (nieatomowy wyścig limitu begin/commit)
  * `make pairing-idempotency-negative`
  * `make pairing-refresh-negative`
  * `make pairing-refresh-race-negative`

### Korelacja śladu / idempotencja wejścia

**Twierdzenie:** przyjmowanie zdarzeń powinno zachowywać korelację śladu podczas rozsyłania i być idempotentne przy ponowieniach dostawcy.

Co to oznacza:

* Gdy jedno zdarzenie zewnętrzne staje się wieloma wiadomościami wewnętrznymi, każda część zachowuje tę samą tożsamość śladu/zdarzenia.

* Ponowienia nie skutkują podwójnym przetwarzaniem.

* Jeśli brakuje identyfikatorów zdarzeń dostawcy, deduplikacja wraca do bezpiecznego klucza (np. identyfikatora śladu), aby uniknąć odrzucania odrębnych zdarzeń.

* Zielone:
  * `make ingress-trace`
  * `make ingress-trace2`
  * `make ingress-idempotency`
  * `make ingress-dedupe-fallback`

* Czerwone (oczekiwane):
  * `make ingress-trace-negative`
  * `make ingress-trace2-negative`
  * `make ingress-idempotency-negative`
  * `make ingress-dedupe-fallback-negative`

### Pierwszeństwo dmScope routingu + identityLinks

**Twierdzenie:** routing musi domyślnie izolować sesje DM i łączyć sesje tylko wtedy, gdy zostało to jawnie skonfigurowane (pierwszeństwo kanału + linki tożsamości).

Co to oznacza:

* Nadpisania dmScope specyficzne dla kanału muszą mieć pierwszeństwo przed globalnymi wartościami domyślnymi.

* identityLinks powinny łączyć tylko w ramach jawnie powiązanych grup, a nie między niepowiązanymi nadawcami.

* Zielone:
  * `make routing-precedence`
  * `make routing-identitylinks`

* Czerwone (oczekiwane):
  * `make routing-precedence-negative`
  * `make routing-identitylinks-negative`

## Powiązane

* [Model zagrożeń](/pl/security/THREAT-MODEL-ATLAS)
* [Współtworzenie modelu zagrożeń](/pl/security/CONTRIBUTING-THREAT-MODEL)