Google DeepMind, AlphaProof Code ile Signal protokolünü resmi olarak doğruladı
Google DeepMind araştırmacıları, AI ajanlarını yönlendirerek Signal protokolünün arkasındaki gerçek kodun temel güvenlik özelliklerini matematiksel olarak kanıtladı. Şirket, bunun yaygın olarak konuşlandırılmış bir kriptografik protokolün uygulamasının ilk kez resmi olarak doğrulanması olduğunu iddia ediyor.
Signal'in gerçek kodu matematiksel olarak kanıtlandı
Google DeepMind araştırmacıları, Signal protokolünün arkasındaki gerçek kodun temel güvenlik özelliklerini matematiksel olarak kanıtlamak için AI ajanlarını yönlendirdi. Signal, Signal ve Google Messages gibi uygulamalarda milyarlarca özel konuşmayı koruyan teknolojinin temelini oluşturuyor.
Google DeepMind, çalışmalarının AI'nın bu derinlikte yaygın olarak konuşlandırılmış bir kriptografik protokolü resmi olarak doğrulamak için ilk kez kullanıldığını iddia ediyor. Şirket ayrıca bunun, AI ile veya AI olmadan herhangi bir yöntemle yaygın olarak konuşlandırılmış bir protokolün uygulamasının ilk kez resmi olarak doğrulandığı anlamına geldiğini belirtiyor.
AlphaProof Code nasıl çalışıyor?
Bu sonuç, insan uzmanlığını AI ajanlarıyla birleştiren yeni bir agentic çerçeve olan AlphaProof Code ile elde edildi. Çerçeve, resmi doğrulama işini bir araştırma ekibinin yapacağı şekilde bölen çoklu LLM agentic bir yapıya sahip. İnsan uzmanlar neyin kanıtlanacağına karar veriyor, bir grup AI ajanı da bunu yapıyor.
Araştırmacılar, Signal'in güvenlik hedeflerini resmi matematiksel spesifikasyonlara çevirmek için bir model karışımıyla işbirliği yaptı ve insan uzmanlar her bir resmi spesifikasyonu gözden geçirdi. Kanıtlar, Gemini Carbon tarafından desteklenen ajanlar tarafından üretildi; ajanlar Lean dilinde altı milyondan fazla satır kod yazdı.
Ardından ajanlar kanıtı denetledi ve insan tarafından ikinci bir bakış gerektiren alanları vurguladı. İnsan incelemesi gerektiren alanlar kod tabanının yalnızca yüzde birini oluşturdu. Lean geri kalanı otomatik olarak kontrol eder, böylece uzmanlar insan yargısının en önemli olduğu yere odaklanabilir. AlphaProof Code'da her kanıt, ajanların çalışmasını doğrulamak için Lean tarafından kontrol edilir.
Tasarım düzeyinin ötesine geçen doğrulama
Çoğu protokol doğrulaması tasarım düzeyinde dururken, bu çalışma derlenmiş kodun cihazlarda çalışan tam koda kadar güvenlik özelliklerini yerine getirdiğini kanıtladı. Kanıtlanan güvenlik özellikleri arasında mesajların bir cihaz geçici olarak ele geçirilmeden önce ve sonra korunması yer alıyor.
Gerçek dünya güvenlik açıkları sıklıkla tasarım ile uygulama arasındaki boşlukta saklandığından, bu boşluğu kapatmak kanıtları çok daha karmaşık hale getiriyor. Doğrulama süreci bu karmaşıklığa rağmen yalnızca dört hafta sürdü; bu görev tarihsel olarak uzman ekipler için yıllar alıyordu.
Hatalı kod testi ve açık kaynak adımı
AlphaProof Code'un doğru kodu hatalı koddan ayırt edebildiğini doğrulamak için ekip, daha önce düzeltilmiş iki gerçek hatayı Signal kodunun izole bir sürümüne yeniden yerleştirdi. Her iki durumda da sistem, hatalı sürümün güvensiz olduğuna dair makine tarafından kontrol edilen bir kanıt üretti.
AlphaProof Code'da AI ajanları kullanıcıların bir spesifikasyon yazmasına yardımcı olur ve ardından uygulamanın bu spesifikasyonu karşıladığını özerk olarak kanıtlar. Google DeepMind, resmi doğrulama artefaktlarını açık kaynak olarak yayımlıyor.
Signal CTO'sundan değerlendirme
Signal CTO'su Ehren Kret, AI ajanlarının canlı kodu geçerli Lean teoremlerine dönüştürmesini büyük bir atılım olarak nitelendiriyor. Kret, Signal protokol uygulamasının titizlikle doğrulanmasının kodlarının gizlilik garantilerine daha fazla güven sağladığını belirtiyor.
Google DeepMind, bu başarının AI'nın işletmelere, hükümetlere ve kritik altyapıya elit güvenlik güvencesi sunabileceğini gösterdiğini iddia ediyor. Şirket, bu tekniklerin ölçeklendirilmesinin sürekli araştırma gerektirdiğini de belirtiyor.
