Signal'in Şifreleme Kodu Yapay Zekâyla Matematiksel Olarak Sınandı

Bir şifreleme protokolünün tasarımının sağlam olduğunu söylemek bir şey, o tasarımı çalıştıran gerçek kodun da sağlam olduğunu kanıtlamak başka bir şey. Google DeepMind 10 Kasım 2026'da ikincisine uzanan bir çalışma yayımladı: Signal'in mesajlaşma protokolünü uygulayan kütüphanenin derlenmiş hâli, yani cihazda çalışan makine kodu, bazı güvenlik özellikleri bakımından matematiksel olarak kanıtlandı. Ekip işi dört haftada, yapay zekâ ajanlarının yazdığı yaklaşık 6,5 milyon satırlık kanıtla bitirdi.

Haber, Ars Technica'da WIRED'dan yeniden yayımlandı. WIRED'ın özgün başlığı Signal protokolünün güvenli olduğunu kanıtladığını söylüyor; oysa DeepMind'ın kendi makalesi, neyin kanıtlandığını ve neyin dışarıda bırakıldığını ayrıntılı yazıyor. Bu yazıda önce bu sınırlara bakıyoruz, çünkü haberin değeri onlarda gizli.

Biçimsel doğrulama: testten farkı ne?

Yazılım genellikle testle, kod incelemesiyle ve hata avıyla güvence altına alınır. Bunların ortak sınırı şu: yalnızca bakılan yerde hata bulabilirler. Biçimsel doğrulama (formal verification) ise önce yazılımın sağlaması gereken özelliği matematiksel bir ifade olarak yazar, sonra bu ifadenin kod için her koşulda doğru olduğunu kanıtlar. DeepMind makalesinin deyişiyle böyle bir kanıt, o özelliği bozacak her hatayı ve her yolu dışarıda bırakır.

Bedeli ağırdır. Makalede verilen örneklere göre, biçimsel doğrulamanın en büyük başarı öyküsü sayılan işletim sistemi çekirdeği projesi yirmi kişi-yıl, CompCert derleyicisininki altı kişi-yıl sürdü. Üstelik bu projelerde kod, doğrulanmak üzere özel olarak yazılmıştı. Hâlihazırda üretimde çalışan, derleyiciden geçmiş hazır bir kodu doğrulamak ise kanıtı kolaylaştırmak için koda dokunamadığınız için daha da zordur.

Burada kanıtlar Lean adlı bir dille yazıldı. Lean, bir kanıtın her adımını küçük bir çekirdekle denetleyen bir kanıt yardımcısıdır: kanıt ya tutar ya tutmaz, "neredeyse doğru" diye bir şey yoktur. Bu yüzden kanıtı yazanın güvenilir olması gerekmez; DeepMind bu özelliğe dayanıyor ve kanıtları yazan yapay zekâ ajanlarının hata yapmasının sonucu bozmayacağını, çünkü Lean'in hatalı kanıtı reddedeceğini söylüyor.

Signal protokolü kabaca nasıl çalışır

Signal protokolü uçtan uca şifreli mesajlaşmanın fiilî standartlarından biri. Makaleye göre protokolün değişik biçimleri yalnız Signal uygulamasında değil, WhatsApp'ta, Meta'nın Messenger uygulamasında ve Google Messages'ta da kullanılıyor. Bir oturum iki aşamadan oluşur.

El sıkışma (handshake). Ali, çevrimdışı olan Veli'ye mesaj atmak istiyor. Veli sunucuya önceden birkaç genel anahtar, yani "ön anahtar" (prekey) bırakmıştır. Ali bunlarla Diffie-Hellman denen yöntemle Veli'yle ortak bir sır üretir: dışarıdan bakan biri iki genel anahtardan bu sırrı çıkaramaz. Signal'in el sıkışması olan PQXDH, birkaç Diffie-Hellman değerini bir de kuantum bilgisayarlara dayanıklı bir anahtar kapsülleme yöntemiyle (KEM) karıştırır. Makaleye göre amaç, anahtarlardan bazıları sızsa bile ve el sıkışmayı kaydeden biri ileride kuantum bilgisayara kavuşsa bile sırrın korunmasıdır. Bu sürümde PQXDH hâlâ Kyber1024 kullanıyor; makale bunun ML-KEM-1024 standardının öncülü olduğunu belirtiyor.

Mandal (ratchet). El sıkışmadan çıkan sır, her mesaj için yeni bir anahtar üretmekte kullanılır. Signal buna Triple Ratchet diyor: klasik Double Ratchet ile "seyrek kuantum sonrası mandal" (SPQR) birleşimi. Mandal benzetmesi yerinde: her mesaj anahtarı bir öncekinden tek yönlü bir işlemle türetilir ve kullanıldıktan sonra silinir, geri çevrilemez. Bu sayede bir cihazın anahtarları ele geçse bile eski mesajlar açılamaz; buna ileri gizlilik (forward secrecy) denir. Her yanıtta karışan yeni Diffie-Hellman değeri ise anahtarı çalan tarafı yeniden dışarıda bırakır; yeter ki o yeni değişim sırasında pasif kalsın. Bu da ihlal sonrası güvenlik (post-compromise security) olarak adlandırılıyor.

Tam olarak ne kanıtlandı?

DeepMind, libsignal'in birebir (iki kişilik) oturum kodunu hedef aldı: PQXDH ile oturum kurma ve Triple Ratchet ile mesajlaşma. Kodu değiştirmeden küçük bir komut satırı aracına bağladı, standart Rust derleyicisiyle 64 bitlik Arm (AArch64) makine koduna çevirdi ve teoremleri bu çalıştırılabilir dosyanın kendisi hakkında kurdu. Neden önemli: gerçek hatalar çoğunlukla tasarımla uygulama arasındaki boşlukta, plan ile inşa edilen bina arasındaki farkta çıkar. Önceki doğrulama çalışmalarının çoğu planı inceledi; bu çalışma binaya yöneldi.

Hedef kod	libsignal-protocol 0.105.4 (SPQR 1.6.0 ile), birebir oturumlar
Kanıtlanan işlemler	Oturum başlatma, mesaj gönderme, mesaj alma
Kanıtlanan özellikler	İleri gizlilik, ihlal sonrası güvenlik, mesaj gizliliği ve kimlik doğrulama, el sıkışma gizliliği
Kanıt biçimi	İki ayrı model: sembolik (şifreleme "kusursuz kara kutu" sayılır) ve hesaplamalı (rakibin başarı olasılığı alttaki primitiflerin zorluğuna bağlanır)
Hacim	Yaklaşık 6,5 milyon satır makine denetimli Lean kanıtı; okuyup güvenmek gereken tanımlar yaklaşık 18 bin satır, buna ek olarak yaklaşık 8 bin satırlık makine kodu anlambilimi
Emek	Beş kişilik ekip, dört hafta; bir kanıt turunda tipik olarak 40-80 ajan, tek makinede 24-72 saat

Veriler DeepMind'ın makalesinden ve blog yazısından derlendi. DeepMind, blogunda bunu "yaygın kullanılan bir şifreleme protokolünün bu derinlikte yapay zekâyla doğrulandığı ilk örnek" olarak niteliyor; ayrıca uygulamanın herhangi bir yöntemle, yapay zekâlı ya da yapay zekâsız, doğrulandığı ilk örnek olduğunu öne sürüyor. Bunlar şirketin kendi iddiaları. Makalenin kendisi, daha önce Signal protokolünün doğrulama için sıfırdan yazılmış ayrı bir sürümünün (LibSignal*) bulunduğunu da anıyor; farkı, o çalışmanın üretimdeki libsignal'i hedeflememesi.

Kapsam dışında kalanlar

Makalenin sınırlar bölümü, manşetlerdeki "Signal kanıtlandı" ifadesini epeyce daraltıyor:

• Uygulamanın tamamı yok. Signal mobil uygulaması doğrulanmadı; WIRED da bunu vurguluyor. Grup mesajlaşması makalede "gelecek iş" olarak bırakılmış. Anahtar üretme adımı (keygen) kanıtlanmadı; teoremler anahtarların hazır verildiğini varsayıyor.
• Yan kanallar yok. Yan kanallar ve bellekteki diğer sırlar kapsam dışı. Modelde yalnızca uzun vadeli sırların, ön anahtar sırlarının ve o anki oturumun anahtarlarının sızabileceği varsayılıyor.
• Şifreleme primitifleri sorgulanmadı. SHA-256, AES-256-CBC, X25519, Kyber1024, ML-KEM-768 gibi düşük seviyeli yordamlar kanıtlanmadı; 37 yordam "sözleşme" denen idealleştirilmiş tanımlarla değiştirildi. Sonuçlar bu primitiflerin güvenli olduğu varsayımına bağlı. Makale bunu açıkça yazıyor.
• Senaryo dar. Gerçek sunucu ve kimlik doğrulama altyapısı yok: iki dürüst taraf, doğru anahtar dağıtımı varsayılıyor. Tek seferlik Kyber ön anahtarları ve ilk kullanımda güven (trust-on-first-use) yolu da kapsam dışı.
• Kuantum konusunda iki ayrı durum. Hesaplamalı kanıt yalnız klasik rakipleri kapsıyor. Sembolik kanıt ise el sıkışma gizliliğini, Diffie-Hellman'ı sonradan kırabilen bir rakibe karşı da gösteriyor. Ancak makale, mandal teoremlerinin Triple Ratchet'in Double Ratchet'ten "daha zayıf olmadığını" gösterdiğini, SPQR'nin getirdiği kuantum sonrası "iyileşmeyi" göstermediğini açıkça belirtiyor.
• Güven tabanı var. Teoremlere güvenmek için Lean'e, Arm makine kodunun Lean'deki modeline (467 komut ve 31 sistem çağrısı) ve yazılan spesifikasyonun kendisine güvenmek gerekiyor. Spesifikasyon otomatik denetlenemiyor; hatalı yazılmışsa teorem kodun doğruluğunu değil yanlış soruyu kanıtlamış olur. Makine kodu modeli, Unicorn emülatörü ve Arm'ın resmî belirtiminden türeyen Sail modeliyle sınanmış. Rust derleyicisine ise güvenmek gerekmiyor, çünkü kanıt derlenmiş dosya üzerinde kuruluyor.

Sınırlar listesinde bir ayrıntı daha var: makaleye göre libsignal'in aynı yeniden oynatma (replay) mesajıyla ilişkili eski bir ileri gizlilik kaybı senaryosu, sembolik teoremlerle dışlanmıyor; kod gerekli kontrolü yapıyor ama model bunu şart koşmuyor.

Hata yakalayabildiğini nasıl gösterdiler

Yeni bir açık bulunmadı. WIRED'ın aktardığına göre DeepMind analizi, baktığı bölümlerde yeni bir güvenlik açığı saptamadı. Bunun yerine ekip yöntemin gerçekten hata yakaladığını göstermek için Signal'in daha önce bulunmuş ve giderilmiş iki hatasını (Cheval, Jacomme ve Richards'ın bulduğu hatalar) yalıtılmış bir kopyaya yeniden soktu. İkisinde de sistem, bozuk ikili dosyanın güvenlik teoremini ihlal ettiğini gösteren, makinece denetlenen bir kanıt üretti.

İlkinde, yeni oturumda çözülemeyen bir ön anahtar mesajı eski oturumlarla deneniyor; çözülürse yeni oturumun, imzalı ön anahtarın sırrının bir kopyasını taşıyan onaysız durumu kaydediliyordu. İkincisinde el sıkışmayı yanıtlayan taraf, başlatanın X25519 anahtarının geçerli biçimde olup olmadığına bakmıyordu; yeniden oynatılan ve anahtarı bozulmuş bir el sıkışma, aynı ortak sırra sahip ikinci bir oturum yaratabiliyordu.

Daha az duyulan bulgu şu: kanıtları kurarken ekip, daha önce yayımlanmış analizlerde de hatalar buldu. Makaleye göre Double Ratchet'in hesaplamalı analizinde on beş boşluk ya da hata (eksik varsayımlar, rakibin oyunu hileyle bitirebildiği koşullar gibi) bulundu ve kanıt çıkabilsin diye bunlar düzeltildi. Sembolik tarafta Cheval ve arkadaşlarının yayımlanan ProVerif sorgularından birinin, atlanmış mesaj anahtarlarını yanlış mandal sırasında aradığı için alıcı tarafı ileri gizliliğini yayımlandığı hâliyle yanlış kıldığı da belirtiliyor. Yani makine denetimli kanıt, yayımlanmış kâğıt kanıtların da kusurlarını ortaya çıkardı.

Yapay zekâ ne yaptı, insan ne yaptı

Makaleye göre ajanlar kanıtın tamamını yazdı; yazarlardan hiçbiri kanıt kodu yazmadı. Ama "ne kanıtlanacak" sorusu insanlarındı: ekip kapsamı belirledi, literatürden hangi modellerin temel alınacağına karar verdi, güvenliği nasıl ifade edeceklerini onayladı. Spesifikasyon taslakları Gemini 4 Carbon ve Claude Opus 5.5 modelleriyle insanların gözetiminde çıkarıldı; başka bir model ailesinden bir ajan her taslağı kaynak makaleye ve koda sadakat bakımından inceledi. Kanıtları ise Gemini 4 Carbon ajanları üretti. Blogda ajanların kanıtı denetleyip insan bakışı gereken yerleri işaretlediği, bunun kod tabanının yalnızca yüzde biri olduğu yazılı.

Makalenin belki en çarpıcı gözlemi de bu: kanıt ucuzladığında zor olan, doğru şeyi kanıtlamak. Yazarlara göre çabanın çoğu kanıta değil spesifikasyona gitti. DeepMind araştırmacısı Swarat Chaudhuri, WIRED'a şöyle dedi: "Bu sonuçtan çok heyecanlıyız, ancak bunu dünyadaki tüm yazılımlara ölçeklemeden önce katetmemiz gereken uzun bir yol var ve bunu yapmak istiyoruz." Chaudhuri ayrıca hedeflerin de kanıtların da yapay zekâ tarafından üretildiği, testlerin kendi kendine yazıldığı bir "vibe dünyası" istemediklerini, bir orta yol bulunduğunu söyledi.

Signal'in teknoloji sorumlusu Ehren Kret ise açıklamasında şöyle dedi: "Önceki biçimsel doğrulamalar kodun daha küçük bölümlerine odaklanıyordu; Google DeepMind'ın yaklaşımı bunun kayda değer ölçüde genişletilmesine olanak veriyor." WIRED'a göre DeepMind'ın işi hızlı bitirmesinde Signal Vakfı'nın daha önce yaptığı bazı biçimsel doğrulama çalışmalarının da payı var.

Açık sorular

İlk soru maliyet. DeepMind analizi araştırma projesi olarak ücretsiz yaptı; Google maliyeti açıklamadı ve ticari bir doğrulama ürünü ya da hizmeti planlayıp planlamadığı sorusuna yanıt vermedi. Dört haftalık süre etkileyici, ama bu sürede çalışan beş araştırmacının, onlarca ajanın ve kanıt turlarında çalışan makinelerin de hesabı var. Makale de tam derleme sürelerinin saatleri bulabildiğini ve kanıt iyileştirmesine geniş yer olduğunu kabul ediyor.

İkinci soru genelleme: bu yöntem, kriptografi dışındaki yazılımlarda, çok iş parçacıklı ya da dinamik bağlanan programlarda çalışacak mı? Makale, kullanılan makine kodu modelinin iş parçacığı, sinyal ve dinamik bağlamayı kapsamadığını söylüyor; yani böyle bir programı bugün doğrulamak olanaksız. Üçüncüsü bağımsız inceleme: makale DeepMind'ın kendi sitesinde yayımlandı, hakemli bir dergi ya da konferansta değerlendirildiğine dair bir bilgiye rastlamadık; başka ekiplerin spesifikasyonu inceleyip incelemeyeceğini zaman gösterecek. DeepMind kanıtları ve spesifikasyonu açık kaynak olarak yayımladı; bunun amacı tam da bu tür incelemeye kapı açmak.

Günlük hayatta bunun anlamı şimdilik şu: Signal'i kullananlar için bir şey değişmedi; protokolün bazı temel özellikleri, kodun kendisi düzeyinde matematiksel bir ek güvenceye kavuştu. Güvenceyi gerçekten kaç yazılıma taşıyabileceği ise henüz belli değil.

Fotoğraf: David Malone, CC BY 4.0, Wikimedia Commons