Google DeepMind, Signal’ın Şifreleme Kodunu Matematiksel Olarak Doğruladı

Google DeepMind, 10 Kasım 2026’da AlphaProof Code adlı araştırma çerçevesini tanıttı. Şirket, bu sistemi Signal protokolünün kaynak kodunda yer alan bazı güvenlik özelliklerini matematiksel olarak kanıtlamak için kullandığını söylüyor. Çalışma, Signal’ın tüm uygulamasının veya bütün altyapısının hatasız olduğunun kanıtlandığı anlamına gelmiyor; belirli bir kod tabanını ve tanımlanmış özellikleri kapsıyor.

AlphaProof Code neyi doğruladı?

Google araştırmacıları, Signal’ın referans uygulaması libsignal’ın değiştirilmemiş kodundan derlenen AArch64 çalıştırılabilir dosyasını inceledi. Çalışma, Signal’ın PQXDH el sıkışma mekanizması ve Triple Ratchet protokolündeki seçilmiş güvenlik özelliklerine odaklandı. Bunlar; mesaj gizliliği, kimlik doğrulama ve bazı anahtarların açığa çıkmasından sonra iletişim güvenliğinin yeniden kurulması gibi korumalarla ilgili.

Buradaki “matematiksel kanıt”, yapay zekânın güvenli olduğuna dair bir kanaat bildirmesi değil. DeepMind’ın açıklamasına göre ajanlar Lean adlı kanıt sisteminde milyonlarca satır kanıt üretti; Lean’in küçük doğrulama çekirdeği bu kanıtların belirlenen ifadeleri gerçekten karşıladığını kontrol etti. Araştırmacılar ise hangi güvenlik özelliklerinin ispatlanacağını tanımladı ve spesifikasyonları gözden geçirdi. Dolayısıyla süreçte hem yapay zekâ ajanları hem insan uzmanlar yer aldı.

Çalışmanın sınırları neden önemli?

Doğrulama, libsignal kodunun belirli bir derlenmiş sürümünü ve modellenen çalışma ortamını kapsıyor. Signal’ın tüm istemci uygulamalarının her platformdaki davranışını, sunucularını, işletim sistemlerini veya kullanıcı cihazlarını tek seferde kanıtlamıyor. Ayrıca araştırmacılar bazı kriptografik temel bileşenleri kanıtlanmış varsayımlar olarak modele aldı; sonuçlar bu varsayımlar ve kurulan spesifikasyonlar çerçevesinde geçerli.

DeepMind, bilinen ve daha önce düzeltilmiş iki hatayı yalıtılmış bir kopyaya geri eklediğinde sistemin bu hatalı sürümlerde güvenlik özelliklerinin bozulduğunu kanıtlayabildiğini de aktarıyor. Bu, test edilen yöntemin gerçek kusurları yakalayabildiğine dair bir kontrol. Signal’ın güncel sürümünde bu hataların bulunduğu anlamına gelmiyor.

Signal kullanıcıları için ne değişiyor?

Duyuru yeni bir Signal özelliği veya kullanıcıların yüklemesi gereken bir uygulama güncellemesi değil. Yazışma biçimi değişmiyor. Çalışmanın önemi, güvenlik araştırmacılarının karmaşık ve yaygın kullanılan yazılımların belirli özelliklerini makinece denetlenebilir kanıtlarla sınama yöntemini genişletmesi. Bunun başka uygulamalara aktarılabilmesi için her sistemin özellikleri ve çalışma koşulları ayrıca tanımlanıp doğrulanmalı.

Google, AlphaProof Code’un kaynaklarını ve kanıt çalışmalarını kamuya açtığını belirtiyor. Bu araştırmada kullanılan Gemini 4 Carbon modelinin daha geniş erişime açılmasıyla ilgili ayrıntıları Gemini 4 Carbon haberimizde bulabilirsiniz.

Kaynaklar: Google DeepMind’ın AlphaProof Code ve Signal duyurusu ile teknik çalışma ve açık kanıt materyalleri.