Przejdź do głównej treści

Documentation Index

Fetch the complete documentation index at: https://docs.openclaw.ai/llms.txt

Use this file to discover all available pages before exploring further.

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