Google DeepMind, Signal’ın Temel Makine Kodunu Doğrulamak İçin Yapay Zekâ Ajanlarını Kullanıyor

Google DeepMind, 10 Kasım 2026’da AlphaProof Code’u tanıttı; yapay zekâ ajanlarından oluşan ekipler, Signal’ın derlenmiş libsignal kodunda belirlenmiş güvenlik özelliklerine ilişkin makine tarafından denetlenen Lean kanıtları üretti. Beş kişilik araştırma ekibi kanıt çalışmalarını dört haftada tamamladı ve belirtimlerle doğrulama çıktılarını dış incelemeye açtı.

Çalışma, Signal protokolünün tasarımına ilişkin soyut bir modelin ötesine geçerek derlenmiş uygulamasını ele aldı. Araştırmacılar, değiştirilmemiş libsignal v0.105.4 ve SPQR v1.6.0 crate’lerini küçük bir komut satırı test düzeneğine sardı; ardından standart rustc’yi kullanarak statik bağlantılı bir AArch64 Linux yürütülebilir dosyası oluşturdu. Teknik makale, sonucu yaygın olarak kullanılan bir kriptografik protokol uygulamasının değiştirilmemiş kodu için protokol düzeyinde sunulan ilk güvenlik kanıtları olarak tanımlıyor.

AlphaProof Code İş Bölümünü Nasıl Yaptı?

Beş araştırmacı kanıt çalışmaları için dört hafta harcadı; sembolik ve hesaplamalı kanıtlar üzerinde paralel çalışırken ajanları iş istasyonlarında kesintisiz çalıştırdı. Makaleye göre ajanlar, yaklaşık 26.000 satırlık güvenilir belirtimlere ve AArch64 anlambilimine dayanan, makine tarafından denetlenmiş yaklaşık 6,5 milyon satır Lean kanıt kodu üretti.

Özellikleri insanlar seçti; belirsizlikleri ve güvenlik ödünleşimlerini çözüme kavuşturdu, belirtimleri inceledi ve son onay yetkisini elinde tuttu. Gemini 4 Carbon ve Claude Opus 5.5 ile çalışan ajanlar bu belirtimlerin taslaklarını hazırladı ve onları inceledi; incelemeye farklı bir model ailesi de katıldı. Ardından Gemini 4 Carbon ajan ekipleri tüm kanıt kodunu üretti; yazarların hiçbiri kanıt kodu yazmadı. Tipik çalışmalarda, tek bir makinede 24 ila 72 saat boyunca 40 ila 80 ajan kullanıldı. Bir orkestratör ile ekip liderleri kanıt üreten ajanları koordine ederken mimar ve entegratör rolleri ortak kanıt tabanını korudu.

Bir kanıt, ancak Lean çekirdeği tarafından denetlendikten ve bir karşılaştırıcı, yalnızca Lean’in standart aksiyomlarını kullanarak, kanıtın dışarıda tutulan ve insanlarca onaylanan belirtimle —geçişli tüm tanımlar dâhil— eşleştiğini doğruladıktan sonra kabul edildi. Kanıtlar belirtimlerdeki sorunları ortaya çıkardığında ajanlar küçük değişiklikler önerebiliyordu; ancak güvenilen varsayımlardaki değişiklikler için insan onayı veya kullanıcı tarafından belirlenen bir politika gerekiyordu ve değişiklikler gerekçeleriyle birlikte kayda geçiriliyordu. Bu denetim, ajanların ürettiği kanıtlarda belgelenmiş bir riski ele alıyor: belirtim, tanımlarından biri üzerinden dolaylı olarak zayıflatılabilir.

Güvenlik Kapsamı ve Geçmiş Hatalara Yönelik Testler

Doğrulanan hedef, PQXDH el sıkışmasını ve Triple Ratchet mesajlaşmasını kapsayan bire bir oturum koduydu. Araştırmacılar birbirinden bağımsız iki kanıt sunduklarını bildiriyor: idealleştirilmiş kriptografik varsayımlar altında on sembolik teorem ve bir saldırganın avantajını kriptografik varsayımlar ile istatistiksel terimler üzerinden sınırlayan hesaplamalı bir kanıt. Kanıtlanan özellikler arasında, mevcut durum çalındıktan sonra önceki mesajları koruyan ileriye dönük gizlilik; kimlik doğrulama; bir ihlalden sonra toparlanmayı konu alan ihlal sonrası güvenlik; ve el sıkışma gizliliği bulunuyor. Sembolik kanıt ayrıca, daha sonra gerçekleşecek bir Diffie–Hellman kırılmasının ardından el sıkışma gizliliğinin korunmasını da kapsıyor.

Bu belirtimlerin gerçek hataları yakalayıp yakalayamayacağını sınamak için ekip, daha önce giderilmiş ve weak state ile small subgroup olarak bilinen iki libsignal hatasına yönelik düzeltmeleri tersine uyguladı ve değiştirilmiş ikili dosyaları yeniden derledi. Her iki durumda da sembolik güvenlik teoreminin başarısız olduğunu gösteren Lean kanıtları üretti. Herkese açık doğrulama deposu; hesaplamalı, sembolik, ortak ikili dosya ve AArch64 anlambilimi materyallerini birbirinden ayırıyor, ayrıca kanıtların nasıl yeniden oluşturulup bağımsız olarak denetlenebileceğini belgeliyor.

Signal’ın baş teknoloji sorumlusu Ehren Kret, çalışmanın “kodumuzun gizlilik güvencelerine daha da fazla güven duymamızı sağladığını” söyledi.

Sınırlamalar ve Sonraki Adımlar

Bu güvenceler, Signal’ın uygulamalarının tamamını sertifikalandırmaktan çok uzaktır. Araştırmacıların libsignal-cli derlemesinin yeni başlatılmış bir süreç olarak çalıştırılmasını kapsıyor; anahtar üretimi doğrulanmadı, grup mesajlaşması gelecekteki çalışmalara bırakıldı ve yan kanallar ile çoklu cihaz durumu kapsam dışı tutuldu. Düşük seviyeli kriptografik ilkeller ile seçilmiş çıktı ve kitaplık rutinleri güvenilir sözleşmelerle temsil ediliyor. Bu nedenle sonuç; söz konusu sözleşmelere, onaylanmış belirtimlere, Lean çekirdeğine, AArch64 anlambilimine ve ilkellere ilişkin varsayımlara da bağlı.

Makalede, bu iki kanıtın da SPQR’ın eklemek üzere tasarlandığı kuantum sonrası iyileşmeyi kanıtlamadığı belirtiliyor: hesaplamalı teorem klasik saldırganları kapsarken sembolik ratchet teoremleri saldırganın SPQR anahtarlarını seçmesine izin veriyor. Hesaplamalı model ayrıca saldırganın gerçekleştirebileceği bazı eylemleri kısıtlıyor ve mesaj sayısı ile oturum sayısı yeterince büyüdüğünde anlamsız hâle geliyor. Bu sınırlar, makine tarafından denetlenen kanıtları belirli bir dağıtım için güvenlik güvencesi olarak değerlendirmeden önce dışarıdan inceleme yapanların neleri güvenilir kabul etmesi gerektiğini ortaya koyuyor.

Araştırmacıların belirttiği sonraki adımlar; teoremleri güçlendirmek, kanca eklenmiş daha fazla rutini doğrulayıp kriptografik sözleşmeleri doğrulanmış uygulamalara bağlayarak güvenilir tabanı küçültmek ve kapsamı grup mesajlaşması, sealed sender ve sunucu tarafı protokolleri de içerecek şekilde genişletmek. Yeni libsignal sürümlerini dağıtıma çıkmadan önce doğrulama hedefleri ise duyurulmuş bir dağıtım değil, bir araştırma amacıdır.

Sonucun hemen göze çarpan önemi, ortaya koyduğu iş bölümüdür: İspatların oluşturulmasını ajanlar üstlenirken güvence, insanlar tarafından incelenmiş belirtimlere ve açıkça belirtilmiş varsayımlara dayanıyor. İspatların ve kontrol prosedürlerinin yayımlanması, araştırmacılar bu iş akışını libsignal’ın devam eden geliştirme sürecine taşımak için çalışırken dışarıdan inceleme yapanlara bu temeli sınama olanağı sunuyor.