Security
Weryfikacja formalna (modele bezpieczeństwa)
Formalne modele bezpieczeństwa OpenClaw (obecnie TLA+/TLC) dostarczają zweryfikowanego maszynowo uzasadnienia, że określone ścieżki najwyższego ryzyka — autoryzacja, izolacja sesji, kontrolowanie dostępu do narzędzi i bezpieczeństwo w przypadku błędnej konfiguracji — egzekwują zamierzone zasady przy jawnie określonych założeniach.
Uwaga: niektóre starsze linki mogą odwoływać się do poprzedniej nazwy projektu.
Czym to jest
Wykonywalny, ukierunkowany na działania atakującego zestaw testów regresji bezpieczeństwa:
- Każde twierdzenie ma uruchamialną weryfikację modelu w skończonej przestrzeni stanów.
- Wiele twierdzeń ma odpowiadający mu model negatywny, który generuje ślad kontrprzykładu dla realistycznej klasy błędów.
To nie jest dowód, że OpenClaw jest bezpieczny pod każdym względem, ani weryfikacja pełnej implementacji w TypeScript.
Gdzie znajdują się modele
Modele są utrzymywane w osobnym repozytorium: vignesh07/openclaw-formal-models.
Zastrzeżenia
- Są to modele, a nie pełna implementacja w TypeScript — możliwa jest rozbieżność między modelem a kodem.
- Wyniki są ograniczone przestrzenią stanów przeszukiwaną przez TLC. Wynik pozytywny nie oznacza bezpieczeństwa poza modelowanymi założeniami i granicami.
- Niektóre twierdzenia opierają się na jawnych założeniach dotyczących środowiska (na przykład poprawnym wdrożeniu i poprawnych danych wejściowych konfiguracji).
Odtwarzanie wyników
Sklonuj repozytorium modeli i uruchom TLC:
git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Wymagana jest Java 11+ (TLC działa na JVM).# Repozytorium zawiera przypięty plik tla2tools.jar oraz udostępnia bin/tlc i cele Make. make <target>Nie ma jeszcze integracji CI z tym repozytorium; przyszła wersja mogłaby dodać modele uruchamiane w CI z publicznymi artefaktami (śladami kontrprzykładów, dziennikami uruchomień) albo hostowany przepływ pracy „uruchom ten model” dla niewielkich, ograniczonych weryfikacji.
Twierdzenia i cele
Ekspozycja Gateway i błędna konfiguracja otwartego Gateway
Twierdzenie: nasłuchiwanie poza interfejsem loopback bez uwierzytelniania może umożliwić zdalne przejęcie i zwiększa ekspozycję; zgodnie z założeniami modelu token lub hasło blokuje nieuwierzytelnionych atakujących.
| Wynik | Cele |
|---|---|
| Pozytywny | make gateway-exposure-v2, make gateway-exposure-v2-protected |
| Negatywny (oczekiwany) | make gateway-exposure-v2-negative |
Zobacz także docs/gateway-exposure-matrix.md w repozytorium modeli.
Potok wykonywania Node (możliwość o najwyższym ryzyku)
Twierdzenie: exec host=node wymaga (a) listy dozwolonych poleceń Node wraz z zadeklarowanymi poleceniami oraz (b) zatwierdzenia na żywo, jeśli zostało skonfigurowane; w modelu zatwierdzenia są tokenizowane, aby zapobiec ich ponownemu użyciu.
| Wynik | Cele |
|---|---|
| Pozytywny | make nodes-pipeline, make approvals-token |
| Negatywny (oczekiwany) | make nodes-pipeline-negative, make approvals-token-negative |
Magazyn parowania (kontrola wiadomości prywatnych)
Twierdzenie: żądania parowania przestrzegają TTL i limitów oczekujących żądań.
| Wynik | Cele |
|---|---|
| Pozytywny | make pairing, make pairing-cap |
| Negatywny (oczekiwany) | make pairing-negative, make pairing-cap-negative |
Kontrola ruchu przychodzącego (wzmianki i omijanie za pomocą poleceń sterujących)
Twierdzenie: w kontekstach grupowych wymagających wzmianki nieautoryzowane polecenie sterujące nie może ominąć kontroli wzmianek.
| Wynik | Cele |
|---|---|
| Pozytywny | make ingress-gating |
| Negatywny (oczekiwany) | make ingress-gating-negative |
Izolacja routingu i kluczy sesji
Twierdzenie: wiadomości prywatne od różnych rozmówców nie są łączone w tę samą sesję, chyba że zostały jawnie powiązane lub odpowiednio skonfigurowane.
| Wynik | Cele |
|---|---|
| Pozytywny | make routing-isolation |
| Negatywny (oczekiwany) | make routing-isolation-negative |
Modele v1++: współbieżność, ponowienia i poprawność śladów
Kolejne modele, które zwiększają zgodność z rzeczywistymi trybami awarii: nieatomowymi aktualizacjami, ponowieniami i rozsyłaniem wiadomości.
Współbieżność i idempotencja magazynu parowania
Twierdzenie: magazyn parowania egzekwuje MaxPending i idempotencję nawet przy przeplotach operacji — sprawdzenie, a następnie zapis muszą być atomowe lub chronione blokadą, a odświeżenie nie może tworzyć duplikatów. Konkretnie: współbieżne żądania nie mogą przekroczyć MaxPending dla kanału, a powtarzające się żądania lub odświeżenia dotyczące tej samej pary (channel, sender) nie tworzą zduplikowanych aktywnych oczekujących wierszy.
| Wynik | Cele |
|---|---|
| Pozytywny | make pairing-race (atomowe lub chronione blokadą sprawdzanie limitu), make pairing-idempotency, make pairing-refresh, make pairing-refresh-race |
| Negatywny (oczekiwany) | make pairing-race-negative (nieatomowy wyścig limitu między rozpoczęciem a zatwierdzeniem), make pairing-idempotency-negative, make pairing-refresh-negative, make pairing-refresh-race-negative |
Korelacja śladów i idempotencja ruchu przychodzącego
Twierdzenie: pozyskiwanie wiadomości zachowuje korelację śladów podczas rozsyłania i jest idempotentne przy ponowieniach po stronie dostawcy. Gdy jedno zdarzenie zewnętrzne staje się wieloma wiadomościami wewnętrznymi, każda część zachowuje tę samą tożsamość śladu lub zdarzenia; ponowienia nie powodują podwójnego przetwarzania; jeśli brakuje identyfikatorów zdarzeń dostawcy, deduplikacja korzysta z bezpiecznego klucza zastępczego (na przykład identyfikatora śladu), aby uniknąć odrzucenia odrębnych zdarzeń.
| Wynik | Cele |
|---|---|
| Pozytywny | make ingress-trace, make ingress-trace2, make ingress-idempotency, make ingress-dedupe-fallback |
| Negatywny (oczekiwany) | make ingress-trace-negative, make ingress-trace2-negative, make ingress-idempotency-negative, make ingress-dedupe-fallback-negative |
Pierwszeństwo dmScope w routingu i identityLinks
Twierdzenie: routing domyślnie utrzymuje izolację sesji wiadomości prywatnych i łączy sesje wyłącznie po jawnej konfiguracji, zgodnie z pierwszeństwem kanałów i powiązaniami tożsamości. Wartości dmScope właściwe dla kanału mają pierwszeństwo przed globalnymi wartościami domyślnymi; identityLinks łączą sesje wyłącznie w ramach jawnie powiązanych grup, a nie między niepowiązanymi rozmówcami.
| Wynik | Cele |
|---|---|
| Pozytywny | make routing-precedence, make routing-identitylinks |
| Negatywny (oczekiwany) | make routing-precedence-negative, make routing-identitylinks-negative |
