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.
Modellerin bulunduğu yer
Modeller ayrı bir depoda tutulur: vignesh07/openclaw-formal-models.Bu yazının hazırlandığı sırada söz konusu depoya erişilemiyor (GitHub, “Repository not found” yanıtını döndürüyor). Sizin için de hâlâ erişilemiyorsa modellerin kaldırıldığını varsaymadan önce güncel konumu OpenClaw bakım sorumlusu kanallarında sorun.
Uyarılar
- Bunlar TypeScript uygulamasının tamamı değil, modellerdir — model ile kod arasında sapma olması mümkündür.
- Sonuçlar, TLC’nin araştırdığı 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:İddialar ve hedefler
Gateway erişimi ve açık Gateway yanlış yapılandırması
İddia: Modelin varsayımlarına göre, kimlik doğrulama olmadan geri döngü dışına bağlanmak uzaktan ele geçirmeyi mümkün kılabilir ve erişimi genişletir; bir belirteç/parola, kimliği doğrulanmamış saldırganları engeller.
Ayrıca model deposundaki
docs/gateway-exposure-matrix.md bölümüne bakın.
Node yürütme işlem hattı (en yüksek riskli yetenek)
İddia: Modeldeexec host=node; (a) bir Node komutu izin listesi ile bildirilmiş komutları ve (b) yapılandırıldığında canlı onayı gerektirir; yeniden oynatmayı önlemek için onaylar belirteçleştirilir.
Eşleştirme deposu (DM geçitleme)
İddia: Eşleştirme istekleri TTL’ye ve bekleyen istek sınırlarına uyar.Giriş geçitleme (bahsetmeler ve denetim komutu atlaması)
İddia: Bahsetme gerektiren grup bağlamlarında, yetkisiz bir denetim komutu bahsetme geçitlemesini atlayamaz.Yönlendirme ve oturum anahtarı yalıtımı
İddia: Farklı eşlerden gelen DM’ler, açıkça bağlanmadıkları veya bu şekilde yapılandırılmadıkları sürece aynı oturumda birleşmez.v1++ modelleri: eşzamanlılık, yeniden denemeler ve iz doğruluğu
Atomik olmayan güncellemeler, yeniden denemeler ve ileti dağıtımı gibi gerçek dünyadaki hata modlarına ilişkin 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, yürütmeler iç içe geçtiğinde bileMaxPending ve eşgüçlülüğü uygular — denetle-sonra-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 tekrarlanan istekler/yenilemeler, yinelenen etkin bekleyen satırlar oluşturmaz.
Giriş izi korelasyonu ve eşgüçlülük
İddia: İçeri alma işlemi, dağıtım boyunca iz korelasyonunu korur ve sağlayıcının yeniden denemeleri altında eşgüçlüdür. Bir harici olay birden çok dahili iletiye 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 farklı olayların atılmasını önlemek için tekilleştirme güvenli bir anahtara (örneğin iz kimliğine) geri döner.Yönlendirmede dmScope önceliği ve identityLinks
İddia:dmScope önceliği ve kimlik bağlantıları belirlenimci biçimde davranır: varsayılan main kapsamı, tek bir sahibin DM’leri arasında tek bir devreden oturumu paylaşırken (kişisel aracı varsayılanı), yapılandırılmış herhangi bir yalıtıcı kapsam (per-peer, per-channel-peer, per-account-channel-peer) DM oturumlarını kesin biçimde ayrı tutar. Kanala özgü dmScope geçersiz kılmaları, genel varsayılanlara göre önceliklidir; identityLinks, oturumları yalnızca açıkça bağlantılı gruplar içinde birleştirir, ilgisiz eşler arasında birleştirmez. Çok kullanıcılı gelen kutularının yalıtıcı bir kapsamı etkinleştirmesi beklenir (çalışma zamanı güvenlik denetimi, çok kullanıcılı DM trafiği algıladığında bunu önerir).