Google DeepMind'ın AlphaProof Code'u Signal'in libsignal kodunu doğruladı

Test yerine matematiksel kanıt

Yazılım güvenliği genellikle test ve denetimle ölçülür. Bu yöntem sorun bulunmadığını söyleyebilir ama sorun olmadığını garanti etmez. Biçimsel doğrulama ise kodun belirli özellikleri ihlal edemeyeceğini bir teorem gibi kanıtlar; ancak çok pahalıdır. 2009'da doğrulanan seL4 çekirdeği, tek kişilik yaklaşık yirmi yıllık emek gerektirmişti.

AlphaProof Code'da insan uzmanlar neyin kanıtlanacağına karar veriyor, ajanlar kanıtı üretiyor. Araştırmacılar özellikleri Signal üzerine akademik çalışmalara dayanarak belirledi. Gemini 4 Carbon modeliyle çalışan ajanlar, her adımı Lean doğrulayıcısının otomatik denetlediği yaklaşık 6,5 milyon satır kanıt yazdı. Araştırmacıların hiçbiri tek satır kanıt yazmadı.

Kanıtlar, şifreleme anahtarlarını sürekli yenileyen “ratchet” mekanizmasına odaklanıyor. Teknik makaleye göre telefondan anahtarları çalan bir saldırgan eski mesajları okuyamıyor; çünkü her mesaj bir öncekinden türetilen ve ardından silinen anahtarla şifreleniyor. İki taraf yeni mesajlar değiştirdiğinde konuşma yeniden güvenli hâle geliyor ve kimse taraflardan birinin kimliğine bürünemiyor. Yöntemi sınamak için araştırmacılar libsignal'in sonradan düzeltilmiş iki eski hatasını geri getirdi; sistem bu sürümlerin beklenen garantileri sağlamadığını gösterdi.

Sınırlar

Signal'in teknik direktörü Ehren Kret sonucu “büyük bir ilerleme” olarak niteledi. Google ise doğrulamanın yalnızca iki kişilik sohbetleri kapsadığını, temel kriptografik bileşenlerin kusursuz çalıştığını varsayıp bunları doğrulamadığını ve mobil uygulamalara değil, Linux'ta çalışan bir test sürümüne dayandığını belirtiyor.

Yazarlara göre kanıtlar ucuzladıkça asıl zor soru neyin kanıtlanacağı olacak.