Google DeepMind, 10 Kasım 2026’da yayımladığı çalışmada AlphaProof Code adlı çoklu ajan sistemiyle Signal’in şifreleme kütüphanesi libsignal’ın temel güvenlik özelliklerini biçimsel olarak doğruladığını açıkladı. Ekip, protokol seviyesindeki güvenlik garantilerini yaygın kullanılan bir uygulamanın değiştirilmemiş koduna bağlayan ilk ispatlar olduğunu söylüyor (Google DeepMind).
İçindekiler
Tam olarak ne kanıtlandı?
Çalışma Signal’in iki temel parçasına odaklandı: kuantum sonrası el sıkışma protokolü PQXDH ve mesaj anahtarlarını sürekli yenileyen Triple Ratchet. Kanıtlanan özellikler ileri gizlilik (bugün ele geçirilen bir anahtar geçmiş mesajları açmıyor), kimlik doğrulama, ele geçirme sonrası güvenlik ve el sıkışma gizliliği. Doğrulama, libsignal v0.105.4 ve SPQR v1.6.0’dan hiç değiştirilmeden derlenen ARM (AArch64) makine kodu üzerinde yapıldı.
Yani ispat yalnızca protokolün kâğıt üzerindeki tasarımı için değil, telefonlarda gerçekten çalışan derlenmiş kod için geçerli. Ekip ayrıca daha önce düzeltilmiş iki libsignal hatasını koda geri ekleyip ortaya çıkan programın güvenlik teoremlerini ihlal ettiğini de gösterdi; yöntem hatalı kodu gerçekten yakalayabiliyor. Bu çalışmada yeni bir hata bulunmadı.
AlphaProof Code nasıl çalışıyor?
Sistem insanla yapay zekânın birlikte çalışması üzerine kurulu. Önce insan yönlendirmesindeki bir ajan, güvenlik hedeflerini Lean adlı ispat dilinde matematiksel bir şartnameye çeviriyor ve bu şartname insanlar tarafından onaylanıyor. Ardından otonom ispat ajanları devreye giriyor; bir ispat ancak Lean çekirdeği doğruladığında ve onaylı şartnameyle eşleştiği teyit edildiğinde kabul ediliyor. Her ispat kampanyasında tek makinede 40 ile 80 ajan 24 ile 72 saat çalıştı.
The Register’ın aktardığına göre Lean kodunu Gemini Carbon tabanlı ajanlar üretti ve toplamda 6,5 milyon satır makine denetimli ispat çıktı. Ardından bir denetim adımı insan incelemesi gereken bölümleri işaretledi (The Register). Ajanların kullandığı modeli Gemini 4 Carbon yazımızda anlatmıştık.
Neden önemli: 20 yıl yerine 4 hafta
Biçimsel doğrulama yazılımın belli koşullarda hata yapmayacağını matematiksel olarak kanıtlamak demek ve bugüne kadar son derece pahalıydı. seL4 işletim sistemi çekirdeğinin doğrulanması yaklaşık 20 insan yılı sürmüştü. Signal çalışması ise beş kişilik bir ekiple dört haftada tamamlandı (The Register). DeepMind araştırmacısı Swarat Chaudhuri, alanda asıl zor kısmın her zaman ispat olduğunun düşünüldüğünü, ancak bundan sonraki sınırın ispattan çok “neyin kanıtlanacağını doğru tarif etmek” olacağını söyledi.
Kanıtın kapsamadığı şeyler
- Hesaplamalı ispatlar yalnızca klasik saldırganları kapsıyor, kuantum bilgisayarlı saldırganları değil.
- Grup mesajları, çoklu cihaz durumu ve ikiden fazla taraf kapsam dışında.
- Anahtar üretimi doğrulanmadı; anahtarların doğru üretildiği varsayılıyor.
- Kullanılan şifreleme algoritmalarının kendisinin güvenli olduğu kanıtlanmadı, varsayıldı.
- Model iş parçacıklarını, dinamik bağlamayı ve bazı işletim sistemi ayrıntılarını içermiyor.
Signal kullanıcıları için ne değişiyor?
Uygulamada görünür bir değişiklik yok. Çalışma Signal’in temel tasarımının ve gerçek kodunun belirlenen özellikleri sağladığını gösteriyor; bu, uygulamanın her türlü saldırıya karşı güvenli olduğu anlamına gelmiyor. Telefonun ele geçirilmesi ya da sahte bağlantılarla yapılan dolandırıcılıklar bu kanıtın konusu değil. Yapay zekânın siber güvenlikteki diğer yüzünü GPT-6 Cyber haberimizde ele almıştık.
Sıkça Sorulan Sorular
AlphaProof Code nedir?
Google DeepMind’ın yazılımın güvenlik ve doğruluk özelliklerini Lean ispat diliyle biçimsel olarak doğrulayan çoklu ajan sistemi.
Signal’in hangi kısmı doğrulandı?
Kuantum sonrası el sıkışma protokolü PQXDH ve Triple Ratchet’in ileri gizlilik, kimlik doğrulama, ele geçirme sonrası güvenlik ve el sıkışma gizliliği özellikleri.
Bu Signal’in tamamen güvenli olduğu anlamına mı geliyor?
Hayır. Grup mesajları, anahtar üretimi ve kuantum saldırganlar gibi konular kapsam dışında; şifreleme algoritmalarının güvenliği varsayıldı.
Doğrulama ne kadar sürdü?
The Register’a göre beş kişilik ekip dört hafta çalıştı ve ajanlar 6,5 milyon satır Lean ispatı üretti.
Kaynaklar
- AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level (Google DeepMind, 10 Kasım 2026)
- Google DeepMind melds humans and AI agents to vet Signal’s secure messaging techniques (The Register, 10 Kasım 2026)
Daha fazla güncel gelişme için Yapay Zeka Haberleri sayfamıza göz at.
