DeepMind'in AlphaProof Code'u, Signal'ın temel şifrelemesi için makine tarafından doğrulanmış kanıt üretti

Ne oldu

10 Kasım 2026'da Google DeepMind, Signal protokolünün referans implementasyonu olan libsignal'ın resmi bir doğrulamasını yayınladı; bu bir kod incelemesi ya da manuel denetim değil: büyük ölçüde AI tarafından üretilen, cihazlarda gerçekten çalışan derlenmiş kodu kapsayan, makine tarafından doğrulanmış bir matematiksel kanıt.

AlphaProof Code adı verilen proje, beş araştırmacı tarafından dört hafta boyunca yürütüldü. Bu süre zarfında insan gözetiminde çalışan AI ajanları, Lean dilinde altı milyondan fazla satır kanıt üretti. Doğrulama, protokolün kalbindeki iki bileşeni hedefliyor: iki taraf arasında güvenli bir görüşme kuran PQXDH el sıkışması ve her mesaj için anahtarları döndüren Triple Ratchet. libsignal, Signal'ın kendi uygulamasının背后的 kütüphanesidir ve aynı protokol tasarımı WhatsApp ve Google Messages tarafından da kullanılır.

Kodu kanıtlamak, makaleyi değil

dev.to yazarının da belirttiği gibi, sektördeki güvenlik güvencesinin çoğu tasarım seviyesinde kalır. Kriptograflar kâğıt üzerinde tanımlanmış bir protokolün özelliklerini kanıtlar, ardından mühendisler onu implemente eder ve ikisi arasındaki boşluk, implementasyon hatalarının yaşadığı yerdir — yeniden kullanılmış bir nonce, bir hata yolunda atlanan bir adım, makalenin hiç düşünmediği bir durum geçişi.

DeepMind'ın çalışması bildirildiğine göre daha da ileri giderek, derlenmiş kodu ARM cihazlarında çalışan tek tek talimatlara kadar doğruluyor. Dört özellik kanıtlandı: mesajlar gizli kalıyor, karşı taraf kimliği doğrulanıyor, sonraki bir anahtar sızsa bile geçmiş mesajlar gizliliğini koruyor (forward secrecy) ve bir ihlalden sonra görüşme güvenliğini geri kazanıyor (post-compromise security). DeepMind bunu, yaygın olarak dağıtılmış bir protokolün implementasyonunun herhangi bir yöntemle — AI ile ya da AI'sız — ilk kez resmi olarak doğrulanması olarak tanımlıyor.

Başarısız olabilen bir araç

Hata bulmayan bir kanıt bariz bir soruyu davet eder: bir hata varsa yakalar mıydı? dev.to gönderisine göre DeepMind bunu doğrudan test etti: daha önce eski Signal sürümlerinde bulunup düzeltilmiş iki gerçek hatayı kodun izole bir kopyasına yeniden yerleştirdi. Her iki durumda da AlphaProof Code, hatalı sürümün güvensiz olduğuna dair makine tarafından doğrulanmış bir gösterim üretti.

İnsanlar süreçte merkezi olmaya devam etti. Araştırmacılar ve modeller resmi spesifikasyonları birlikte yazdı ve insan uzmanlar her birini inceledi. Ajanlar kod tabanının yaklaşık yüzde birini ikinci bir insan incelemesi için işaretledi, geri kalanını ise Lean otomatik olarak kontrol etti.

Kanıtın kapsamadığı şeyler

dev.to makalesi sınırlar konusunda dikkatli. Kanıt yalnızca birebir oturumları kapsıyor; grup mesajlaşması gelecek çalışma olarak listeleniyor. Doğrulama, ARM Linux için derlenmiş ve bir test ortamında çalışan libsignal 0.105.4 sürümüne uygulanıyor — tam Signal uygulamasına, sunucularına ya da kullanıcı arayüzüne değil. ML-KEM ve eğri aritmetiği gibi düşük seviyeli kriptografik yapı taşları kanıtlanmak yerine güvenli varsayılıyor. Ve herhangi bir kanıt spesifikasyonuna dayanır: yanlış bir güvenlik hedefi yazılırsa, kanıtlayıcı yalnızca yanlış iddiayı doğrular.

Bir de kapsam uyarısı var. WhatsApp ve Google Messages, Signal protokolünün kendi implementasyonlarını sürdürüyor; dolayısıyla sonuç, fikirlerini ödünç alan her uygulamaya otomatik olarak taşınmıyor.

Neden önemli

Beş kişilik bir ekip dört hafta içinde dağıtılmış bir protokolün implementasyon seviyesinde doğrulamasını üretebiliyorsa, resmi doğrulama çarpıcı biçimde ucuzluyor demektir. Bu tür çalışmalar tarihsel olarak uzman ekiplerin yıllarını almış ve yalnızca en büyük kuruluşların erişimine açık olmuştur. DeepMind doğrulama artefaktlarını açık kaynak olarak yayınladı, "Formal Verification of Signal's Protocol with Gemini" başlıklı teknik bir makale yayınladı ve tıbbi cihaz donanım yazılımı ile elektrik şebekesi yazılımını gelecek hedefler olarak gösterdi.

Mesajlaşma geliştiricileri için daha yakın etki, bir sonraki protokol neslinin — post-quantum tasarımlar dahil — baştan itibaren implementasyon derinliğinde doğrulanabilmesi, yıllar sonra denetlenmek yerine. AI hem kod üretimi hem de koda yönelik saldırıları hızlandırırken, dev.to yazarının savunduğu gibi, haftalar içinde doğrulanabilen savunmalar, ayak uydurabilen savunmalardır. DeepMind ayrıca doğrulamayı CodeMender adlı bir araçla otomatik yamalamayla eşleştirmeyi öneriyor; bu da keşfedilen hatadan kanıtlanmış düzeltmeye giden döngünün sürüm döngüleriyle değil haftalarla ölçülebileceğine işaret ediyor.

Bunların hiçbiri Signal uygulamasının tamamını güvenli kılmıyor ve denetimler eskimiş değil. Ama yazılım için mevcut en güçlü güvence biçimi artık bir mesajlaşma uygulamasının en çok önemli olduğu kısmına uygulandı ve mevcut kodda yeni bir kusur bulunmadı. DeepMind'ın ifadesine göre, bu düzeydeki doğrulama çok yıllı bir araştırma çabasından küçük bir ekibin planlayabileceği bir şeye dönüştü.