Security
Biçimsel doğrulama (güvenlik modelleri)
OpenClaw'ın biçimsel güvenlik modelleri (günümüzde TLA+/TLC), açıkça belirtilen varsayımlar altında en yüksek risk taşıyan belirli yolların — yetkilendirme, oturum yalıtımı, araç geçitleme ve yanlış yapılandırma güvenliği — amaçlanan politikayı uyguladığına dair makine tarafından denetlenmiş bir gerekçe sunar.
Not: Bazı eski bağlantılar önceki proje adına atıfta bulunabilir.
Bu nedir?
Yürütülebilir, saldırgan odaklı bir güvenlik regresyon paketi:
- Her iddia, sonlu bir durum uzayı üzerinde çalıştırılabilir bir model denetimine sahiptir.
- Birçok iddianın, gerçekçi bir hata sınıfı için karşı örnek izi üreten eşleştirilmiş bir negatif modeli vardır.
Bu, OpenClaw'ın her açıdan güvenli olduğunun kanıtı değildir ve TypeScript uygulamasının tamamını doğrulamaz.
Modellerin bulunduğu yer
Modeller ayrı bir depoda tutulur: vignesh07/openclaw-formal-models.
Sınırlamalar
- Bunlar modeldir, TypeScript uygulamasının tamamı değildir; model ile kod arasında sapma olması mümkündür.
- Sonuçlar, TLC'nin incelediği durum uzayıyla sınırlıdır. Yeşil sonuç, modellenen varsayımların ve sınırların ötesinde güvenlik anlamına gelmez.
- Bazı iddialar açık ortam varsayımlarına dayanır (örneğin doğru dağıtım ve doğru yapılandırma girdileri).
Sonuçları yeniden üretme
Model deposunu klonlayın ve TLC'yi çalıştırın:
git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Java 11+ gerekli (TLC, JVM üzerinde çalışır).# Depo, sabitlenmiş bir tla2tools.jar sürümünü içerir ve bin/tlc ile Make hedefleri sağlar. make <target>Henüz bu depoya yönelik bir CI entegrasyonu yoktur; gelecekteki bir sürüm, herkese açık yapıtlarla (karşı örnek izleri, çalıştırma günlükleri) CI tarafından çalıştırılan modeller veya küçük ve sınırlı denetimler için barındırılan bir "bu modeli çalıştır" iş akışı ekleyebilir.
İddialar ve hedefler
Gateway erişimi ve açık Gateway yanlış yapılandırması
İddia: Kimlik doğrulama olmadan loopback ötesine bağlanmak, uzaktan ele geçirmeyi mümkün kılabilir ve erişim kapsamını artırır; modelin varsayımlarına göre bir belirteç/parola, kimliği doğrulanmamış saldırganları engeller.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make gateway-exposure-v2, make gateway-exposure-v2-protected |
| Kırmızı (beklenen) | make gateway-exposure-v2-negative |
Model deposundaki docs/gateway-exposure-matrix.md dosyasına da bakın.
Node exec işlem hattı (en yüksek riskli yetenek)
İddia: Modelde exec host=node, (a) bir Node komutu izin listesi ile bildirilmiş komutları ve (b) yapılandırıldığında canlı onayı gerektirir; yeniden oynatma saldırılarını önlemek için onaylar belirteçleştirilir.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make nodes-pipeline, make approvals-token |
| Kırmızı (beklenen) | make nodes-pipeline-negative, make approvals-token-negative |
Eşleştirme deposu (DM geçitleme)
İddia: Eşleştirme istekleri TTL'ye ve bekleyen istek sınırlarına uyar.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make pairing, make pairing-cap |
| Kırmızı (beklenen) | make pairing-negative, make pairing-cap-negative |
Giriş geçitleme (bahsetmeler ve denetim komutu atlatması)
İddia: Bahsetme gerektiren grup bağlamlarında, yetkisiz bir denetim komutu bahsetme geçitlemesini atlayamaz.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make ingress-gating |
| Kırmızı (beklenen) | make ingress-gating-negative |
Yönlendirme ve oturum anahtarı yalıtımı
İddia: Farklı eşlerden gelen DM'ler, açıkça bağlanmadıkça veya bu şekilde yapılandırılmadıkça aynı oturumda birleştirilmez.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make routing-isolation |
| Kırmızı (beklenen) | make routing-isolation-negative |
v1++ modelleri: eşzamanlılık, yeniden denemeler ve iz doğruluğu
Atomik olmayan güncellemeler, yeniden denemeler ve mesajların çoklu dağıtımı gibi gerçek dünyadaki hata kipleri konusunda doğruluğu artıran devam modelleri.
Eşleştirme deposunda eşzamanlılık ve eşgüçlülük
İddia: Eşleştirme deposu, iç içe geçmeli yürütmeler altında bile MaxPending sınırını ve eşgüçlülüğü uygular; denetle-ve-yaz işlemi atomik/kilitli olmalı ve yenileme yinelenen kayıtlar oluşturmamalıdır. Somut olarak: eşzamanlı istekler bir kanal için MaxPending sınırını aşamaz ve aynı (channel, sender) için yinelenen istekler/yenilemeler, yinelenen etkin bekleyen satırlar oluşturmaz.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make pairing-race (atomik/kilitli sınır denetimi), make pairing-idempotency, make pairing-refresh, make pairing-refresh-race |
| Kırmızı (beklenen) | make pairing-race-negative (atomik olmayan başlatma/işleme sınırı yarış durumu), make pairing-idempotency-negative, make pairing-refresh-negative, make pairing-refresh-race-negative |
Giriş izi korelasyonu ve eşgüçlülük
İddia: İçeri alma işlemi, çoklu dağıtım boyunca iz korelasyonunu korur ve sağlayıcı yeniden denemeleri altında eşgüçlüdür. Bir harici olay birden fazla dahili mesaja dönüştüğünde her parça aynı iz/olay kimliğini korur; yeniden denemeler çift işlemeye yol açmaz; sağlayıcı olay kimlikleri eksikse tekilleştirme, farklı olayların elenmesini önlemek için güvenli bir anahtara (örneğin iz kimliğine) geri döner.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make ingress-trace, make ingress-trace2, make ingress-idempotency, make ingress-dedupe-fallback |
| Kırmızı (beklenen) | make ingress-trace-negative, make ingress-trace2-negative, make ingress-idempotency-negative, make ingress-dedupe-fallback-negative |
Yönlendirmede dmScope önceliği ve identityLinks
İddia: Yönlendirme, DM oturumlarını varsayılan olarak yalıtılmış tutar ve oturumları yalnızca kanal önceliği ve kimlik bağlantıları aracılığıyla açıkça yapılandırıldığında birleştirir. Kanala özgü dmScope geçersiz kılmaları, genel varsayılanlara göre önceliklidir; identityLinks, oturumları ilgisiz eşler arasında değil, yalnızca açıkça bağlanmış gruplar içinde birleştirir.
| Sonuç | Hedefler |
|---|---|
| Yeşil | make routing-precedence, make routing-identitylinks |
| Kırmızı (beklenen) | make routing-precedence-negative, make routing-identitylinks-negative |
