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.

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

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ń
• Współtworzenie modelu zagrożeń