DeepMind'in AlphaProof Code'u, Signal'ın kriptografik protokolünü resmi olarak doğruladı

Google DeepMind, Signal ve Google Messages dahil uygulamalardaki sohbetleri güvence altına alan kod olan Signal'ın kriptografik protokolünün güvenlik özelliklerini matematiksel olarak kanıtlamak için yapay zekâ ajanları kullandığını duyurdu. Şirket, 10 Kasım 2026'da bir blog yazısında açıkladığı bu sonucu, AlphaProof Code adlı yeni bir çerçeveyle elde etti.

DeepMind'a göre bu çalışma, yapay zekânın yaygın şekilde kullanımda olan bir kriptografik protokolü bu derinlikte resmi olarak doğruladığı ilk durum. Şirket ayrıca, böyle bir protokolün soyut tasarımının değil de uygulanmasının (implementation), yapay zekâ ile ya da yapay zekâsız, herhangi bir yöntemle resmi olarak doğrulandığının da ilk kez olduğunu iddia ediyor.

Doğrulama nasıl çalıştı

Resmi doğrulama, kodun amaçlandığı gibi davrandığını matematik kullanarak kanıtlar ve genel olarak mevcut en güçlü güvenlik güvencesi biçimi olarak kabul edilir. Geleneksel olarak o kadar yavaş ve emek yoğundur ki büyük, üretim yazılımlarına nadiren uygulanır.

DeepMind, AlphaProof Code'u emeği bir araştırma grubu gibi bölen çoklu LLM'li ajan tabanlı bir çerçeve olarak tanımlıyor. İnsan uzmanlar, modellerle birlikte çalışarak Signal'ın güvenlik hedeflerini resmi matematiksel belirtimlere çevirdi ve her belirtim bir insan tarafından gözden geçirildi. DeepMind'ın Gemini Carbon adını verdiği bir modelle çalışan ajanlar daha sonra kanıtları yürüttü ve kanıtların mekanik olarak denetlendiği bir dil olan Lean'da altı milyondan fazla satır üretti.

Ajanlar daha sonra kendi çalışmalarını denetledi ve üretilen kod tabanının yalnızca yaklaşık yüzde birini insan incelemesine işaret etti. Lean kalan kısmı otomatik olarak doğruladığı için DeepMind, uzmanlarının yargının en çok önemli olduğu küçük kesime odaklanabildiğini söylüyor.

Kanıtlar kullanımdaki koda genişletildi

DeepMind, kriptografik protokollerin resmi analizinin çoğunun tasarım düzeyinde durduğuna dikkat çekiyor. Ajanları daha ileri giderek, derlenen kodun cihazlarda çalışan tam kod için, bir cihazın geçici olarak ele geçirilmesinden önce ve sonra mesajların korunmaya devam etmesi gibi temel güvenlik özelliklerini karşıladığını gösterdi. Şirket, bu adımın önemli olduğunu, çünkü gerçek sistemlerdeki kusurların sıklıkla tasarımından uygulamaya geçişte ortaya çıktığını ve bu mesafeyi kapsamanın böyle kanıtları bu kadar zorlaştırdığını savunuyor.

Buna rağmen DeepMind'a göre tüm çaba dört hafta sürdü; şirket, karşılaştırılabilir doğrulama çabalarının tarihsel olarak uzman ekiplere yıllar aldığını söylüyor.

Yerleştirilen hatalar yakalandı

Sistemin güvenli kodu bozuk koddan gerçekten ayırt edip edemediğini test etmek için araştırmacılar, Signal'ın kodunun izole bir kopyasına daha önce düzeltilmiş iki gerçek hatayı yeniden yerleştirdi. DeepMind her iki durumda da sistemin, değiştirilmiş sürümün güvensiz olduğuna dair makine onaylı bir kanıt ürettiğini bildiriyor.

Neden önemli

Kriptografik protokoller bankacılıktan gezinmeye kadar neredeyse tüm dijital iletişimin altında yatıyor ve DeepMind, tek bir kusurun aynı anda milyonlarca insanı açıkta bırakabileceğine dikkat çekiyor. Şimdiye kadar bu tür kodların matematiksel kanıtı yaygın kullanılan yazılımlar için erişilemezdi. DeepMind'ın sonuçları geçerliyse, makine onaylı doğrulama en çok ihtiyaç duyan sistemler için pratik hale gelebilir ve Signal kullanıcıları, protokolün gizlilik iddialarının gerçekten sevk edilen kodda geçerli olduğuna dair daha güçlü bir güvence kazanır.

DeepMind ayrıca bu sonucu, yapay zekâ güdümlü saldırıların geleceğine bir hazırlık olarak çerçeveliyor ve otomatik teorem kanıtlamanın CodeMender aracı gibi savunma ajanlarıyla eşleştirildiğinde modern tehditlerin hızına ve ölçeğine ayak uydurabileceğini savunuyor.

Açık yapaylar ve açık sorular

Şirket, resmi doğrulama yapaylarını (artifact) açık kaynak yapıyor ve teknik bir makale yayımladı. Bu tekniklerin daha fazla ölçeklenmesinin sürdürülen araştırma gerektireceği konusunda uyarıyor ve yaklaşımın sonunda tıbbi cihaz yazılımından elektrik şebekesi sistemlerine kadar diğer kritik yazılımları güvence altına alabileceğini öneriyor. Yazıya göre Signal araştırmacıları Rolfe Schmidt, Michael Rosenberg ve Ehren Kret metodoloji hakkında geri bildirim sağladı, ancak doğrulama çalışmasının kendisi DeepMind'ın ekibi tarafından yürütüldü.